MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp11 Structured version   Visualization version   GIF version

Theorem simp11 1222
Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
Assertion
Ref Expression
simp11 (((𝜑𝜓𝜒) ∧ 𝜃𝜏) → 𝜑)

Proof of Theorem simp11
StepHypRef Expression
1 simp1 1128 . 2 ((𝜑𝜓𝜒) → 𝜑)
213ad2ant1 1125 1 (((𝜑𝜓𝜒) ∧ 𝜃𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1074
This theorem is referenced by:  simpl11  1285  simpr11  1294  simp111  1339  simp211  1348  simp311  1357  funcnvqpOLD  6066  omeulem1  7782  omeu  7785  ackbij1lem16  9170  coprimeprodsq  15636  pythagtriplem14  15656  pythagtrip  15662  mrelatglb  17306  subglsm  18207  lsmpropd  18211  mdetmul  20552  decpmatid  20698  isfil2  21782  filuni  21811  cxple2a  24565  isosctr  24671  brbtwn2  25905  colinearalg  25910  ax5seglem3  25931  clwwlknonex2  27179  measres  30515  bayesth  30731  nolesgn2o  32051  nolesgn2ores  32052  nolt02o  32072  ofscom  32341  btwndiff  32361  ifscgr  32378  brofs2  32411  brifs2  32412  fscgr  32414  btwnconn1lem1  32421  btwnconn1lem2  32422  btwnconn1lem3  32423  btwnconn1lem4  32424  btwnconn1lem5  32425  btwnconn1lem6  32426  btwnconn1lem7  32427  btwnconn1lem8  32428  btwnconn1lem9  32429  btwnconn1lem10  32430  btwnconn1lem11  32431  btwnconn1lem12  32432  seglecgr12im  32444  seglecgr12  32445  ivthALT  32557  eqlkr  34806  lkrshp  34812  lshpkrlem5  34821  cvrval3  35119  4noncolr3  35159  4noncolr2  35160  4noncolr1  35161  athgt  35162  3dimlem2  35165  3dimlem3a  35166  3dimlem4a  35169  3dimlem4  35170  3dimlem4OLDN  35171  3dim2  35174  1cvratex  35179  hlatexch4  35187  ps-2b  35188  3atlem1  35189  3atlem2  35190  3atlem4  35192  3atlem5  35193  3atlem6  35194  llnnleat  35219  2atm  35233  ps-2c  35234  llnmlplnN  35245  lplnnlelln  35249  2atmat  35267  2llnjN  35273  lvoli2  35287  lvolnlelln  35290  4atlem3b  35304  4atlem9  35309  4atlem10a  35310  4atlem10  35312  4atlem11a  35313  4atlem11b  35314  4atlem12a  35316  4atlem12b  35317  4at  35319  4at2  35320  lplncvrlvol2  35321  2lplnj  35326  dalemswapyz  35362  dath2  35443  lneq2at  35484  2lnat  35490  cdlema1N  35497  cdlemb  35500  paddasslem15  35540  pmodlem1  35552  llnmod2i2  35569  llnexchb2lem  35574  llnexchb2  35575  dalawlem1  35577  dalawlem3  35579  dalawlem4  35580  dalawlem5  35581  dalawlem6  35582  dalawlem7  35583  dalawlem8  35584  dalawlem9  35585  dalawlem10  35586  dalawlem11  35587  dalawlem12  35588  dalawlem13  35589  dalawlem15  35591  dalaw  35592  osumcllem5N  35666  osumcllem6N  35667  osumcllem7N  35668  osumcllem9N  35670  osumcllem10N  35671  osumcllem11N  35672  pl42lem1N  35685  lhpexle3lem  35717  lhpmcvr5N  35733  lhp2atne  35740  lhp2at0ne  35742  4atexlemswapqr  35769  4atexlemex6  35780  ldilco  35822  ltrneq  35855  trlval2  35870  trlnidat  35880  cdlemd2  35906  cdlemd7  35911  cdlemd8  35912  cdleme7aa  35949  cdleme7c  35952  cdleme7d  35953  cdleme7e  35954  cdleme7ga  35955  cdleme7  35956  cdleme11c  35968  cdleme11e  35970  cdleme11l  35976  cdleme11  35977  cdleme14  35980  cdleme15a  35981  cdleme15c  35983  cdleme16b  35986  cdleme16c  35987  cdleme16d  35988  cdleme16e  35989  cdleme16f  35990  cdleme0nex  35997  cdleme18d  36002  cdleme19b  36011  cdleme19d  36013  cdleme19e  36014  cdleme20f  36021  cdleme20i  36024  cdleme20k  36026  cdleme20l1  36027  cdleme20l2  36028  cdleme20l  36029  cdleme20m  36030  cdleme21a  36032  cdleme21b  36033  cdleme21ct  36036  cdleme21d  36037  cdleme21e  36038  cdleme21f  36039  cdleme21h  36041  cdleme22eALTN  36052  cdleme22f2  36054  cdleme22g  36055  cdleme26e  36066  cdleme26eALTN  36068  cdleme26fALTN  36069  cdleme26f  36070  cdleme26f2ALTN  36071  cdleme26f2  36072  cdleme28a  36077  cdleme28b  36078  cdleme28  36080  cdleme29ex  36081  cdleme29c  36083  cdlemefrs29cpre1  36105  cdlemefr29exN  36109  cdlemefr32sn2aw  36111  cdlemefr29bpre0N  36113  cdlemefr29clN  36114  cdlemefr32fvaN  36116  cdlemefr32fva1  36117  cdlemefs32sn1aw  36121  cdleme43fsv1snlem  36127  cdleme41sn3a  36140  cdleme32fva  36144  cdleme32b  36149  cdleme32d  36151  cdleme32e  36152  cdleme32f  36153  cdleme32le  36154  cdleme35a  36155  cdleme35fnpq  36156  cdleme35b  36157  cdleme35c  36158  cdleme35d  36159  cdleme35e  36160  cdleme35f  36161  cdleme36a  36167  cdleme36m  36168  cdleme37m  36169  cdleme39a  36172  cdleme39n  36173  cdleme40m  36174  cdleme40n  36175  cdleme42e  36186  cdleme42f  36187  cdleme42g  36188  cdleme43bN  36197  cdleme43cN  36198  cdleme43dN  36199  cdleme46f2g2  36200  cdleme46f2g1  36201  cdleme17d2  36202  cdleme48b  36210  cdleme4gfv  36214  cdlemeg49le  36218  cdlemeg46c  36220  cdlemeg46fvaw  36223  cdlemeg46nlpq  36224  cdlemeg46frv  36232  cdlemeg46rgv  36235  cdlemeg46req  36236  cdlemeg46gfre  36239  cdleme50trn1  36256  cdleme50trn2a  36257  cdleme50trn2  36258  cdleme  36267  cdlemf  36270  trlord  36276  cdlemg2ce  36299  cdlemg7fvbwN  36314  cdlemg7aN  36332  cdlemg10bALTN  36343  cdlemg10a  36347  cdlemg10  36348  cdlemg12d  36353  cdlemg12f  36355  cdlemg12g  36356  cdlemg12  36357  cdlemg13a  36358  cdlemg13  36359  cdlemg17b  36369  cdlemg17dN  36370  cdlemg17dALTN  36371  cdlemg17e  36372  cdlemg17f  36373  cdlemg17g  36374  cdlemg17h  36375  cdlemg17i  36376  cdlemg17pq  36379  cdlemg17bq  36380  cdlemg17iqN  36381  cdlemg17  36384  cdlemg18d  36388  cdlemg18  36389  cdlemg19a  36390  cdlemg19  36391  cdlemg21  36393  cdlemg27a  36399  cdlemg28a  36400  cdlemg31b0N  36401  cdlemg27b  36403  cdlemg33b0  36408  cdlemg28b  36410  cdlemg28  36411  cdlemg33a  36413  cdlemg33  36418  cdlemg34  36419  cdlemg35  36420  cdlemg36  36421  ltrnco  36426  trlcone  36435  cdlemg44  36440  cdlemg47  36443  cdlemg48  36444  tendococl  36479  tendoplcl  36488  cdlemh1  36522  cdlemi  36527  cdlemj1  36528  cdlemj2  36529  tendocan  36531  cdlemk6  36544  cdlemki  36548  cdlemksat  36553  cdlemksv2  36554  cdlemk7  36555  cdlemk11  36556  cdlemk12  36557  cdlemkoatnle  36558  cdlemkole  36560  cdlemk14  36561  cdlemk15  36562  cdlemk16a  36563  cdlemk16  36564  cdlemk17  36565  cdlemk1u  36566  cdlemk5u  36568  cdlemk6u  36569  cdlemkuat  36573  cdlemk18  36575  cdlemk19  36576  cdlemk12u  36579  cdlemk21N  36580  cdlemk20  36581  cdlemkoatnle-2N  36582  cdlemk13-2N  36583  cdlemkole-2N  36584  cdlemk14-2N  36585  cdlemk15-2N  36586  cdlemk16-2N  36587  cdlemk17-2N  36588  cdlemk18-2N  36593  cdlemk19-2N  36594  cdlemk7u-2N  36595  cdlemk11u-2N  36596  cdlemk12u-2N  36597  cdlemk21-2N  36598  cdlemk20-2N  36599  cdlemk22  36600  cdlemk23-3  36609  cdlemk25-3  36611  cdlemk26b-3  36612  cdlemk27-3  36614  cdlemk28-3  36615  cdlemk33N  36616  cdlemk37  36621  cdlemky  36633  cdlemk11ta  36636  cdlemkid3N  36640  cdlemk11tc  36652  cdlemk11t  36653  cdlemk45  36654  cdlemk46  36655  cdlemk47  36656  cdlemk48  36657  cdlemk49  36658  cdlemk50  36659  cdlemk51  36660  cdlemk52  36661  cdlemk55b  36667  cdlemkyyN  36669  cdlemk55u1  36672  cdlemk55u  36673  cdlemk39u1  36674  cdlemk39u  36675  cdlemk56  36678  cdleml3N  36685  cdleml4N  36686  cdlemm10N  36826  dihord1  36926  dihord2a  36927  dihord2b  36928  dihord10  36931  dihord11c  36932  dihord2pre  36933  dihord4  36966  dihord5apre  36970  dihmeetlem1N  36998  dihglbcpreN  37008  dihjatc1  37019  dihjatc3  37021  dihmeetlem13N  37027  dihmeetlem20N  37034  baerlem3lem2  37418  baerlem5alem2  37419  baerlem5blem2  37420  hdmap14lem11  37589  hdmap14lem12  37590  monotuz  37925  congmul  37953  congsub  37956  rpnnen3lem  38017  ntrclsiso  38784  ntrclskb  38786  ntrclsk3  38787  wessf1ornlem  39787  infleinf  40003  lincdifsn  42640
  Copyright terms: Public domain W3C validator