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

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

Proof of Theorem simp11
StepHypRef Expression
1 simp1 1159 . 2 ((𝜑𝜓𝜒) → 𝜑)
213ad2ant1 1156 1 (((𝜑𝜓𝜒) ∧ 𝜃𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  simpl11OLD  1323  simpr11OLD  1341  simp111  1394  simp211  1403  simp311  1412  omeulem1  7909  omeu  7912  ackbij1lem16  9352  coprimeprodsq  15750  pythagtriplem14  15770  pythagtrip  15776  mrelatglb  17409  subglsm  18307  lsmpropd  18311  mdetmul  20661  decpmatid  20809  isfil2  21894  filuni  21923  cxple2a  24682  isosctr  24788  brbtwn2  26022  colinearalg  26027  ax5seglem3  26048  clwwlknonex2  27301  measres  30633  bayesth  30849  nolesgn2o  32167  nolesgn2ores  32168  nolt02o  32188  ofscom  32457  btwndiff  32477  ifscgr  32494  brofs2  32527  brifs2  32528  fscgr  32530  btwnconn1lem1  32537  btwnconn1lem2  32538  btwnconn1lem3  32539  btwnconn1lem4  32540  btwnconn1lem5  32541  btwnconn1lem6  32542  btwnconn1lem7  32543  btwnconn1lem8  32544  btwnconn1lem9  32545  btwnconn1lem10  32546  btwnconn1lem11  32547  btwnconn1lem12  32548  seglecgr12im  32560  seglecgr12  32561  ivthALT  32673  eqlkr  34898  lkrshp  34904  lshpkrlem5  34913  cvrval3  35212  4noncolr3  35252  4noncolr2  35253  4noncolr1  35254  athgt  35255  3dimlem2  35258  3dimlem3a  35259  3dimlem4a  35262  3dimlem4  35263  3dimlem4OLDN  35264  3dim2  35267  1cvratex  35272  hlatexch4  35280  ps-2b  35281  3atlem1  35282  3atlem2  35283  3atlem4  35285  3atlem5  35286  3atlem6  35287  llnnleat  35312  2atm  35326  ps-2c  35327  llnmlplnN  35338  lplnnlelln  35342  2atmat  35360  2llnjN  35366  lvoli2  35380  lvolnlelln  35383  4atlem3b  35397  4atlem9  35402  4atlem10a  35403  4atlem10  35405  4atlem11a  35406  4atlem11b  35407  4atlem12a  35409  4atlem12b  35410  4at  35412  4at2  35413  lplncvrlvol2  35414  2lplnj  35419  dalemswapyz  35455  dath2  35536  lneq2at  35577  2lnat  35583  cdlema1N  35590  cdlemb  35593  paddasslem15  35633  pmodlem1  35645  llnmod2i2  35662  llnexchb2lem  35667  llnexchb2  35668  dalawlem1  35670  dalawlem3  35672  dalawlem4  35673  dalawlem5  35674  dalawlem6  35675  dalawlem7  35676  dalawlem8  35677  dalawlem9  35678  dalawlem10  35679  dalawlem11  35680  dalawlem12  35681  dalawlem13  35682  dalawlem15  35684  dalaw  35685  osumcllem5N  35759  osumcllem6N  35760  osumcllem7N  35761  osumcllem9N  35763  osumcllem10N  35764  osumcllem11N  35765  pl42lem1N  35778  lhpexle3lem  35810  lhpmcvr5N  35826  lhp2atne  35833  lhp2at0ne  35835  4atexlemswapqr  35862  4atexlemex6  35873  ldilco  35915  ltrneq  35948  trlval2  35962  trlnidat  35972  cdlemd2  35998  cdlemd7  36003  cdlemd8  36004  cdleme7aa  36041  cdleme7c  36044  cdleme7d  36045  cdleme7e  36046  cdleme7ga  36047  cdleme7  36048  cdleme11c  36060  cdleme11e  36062  cdleme11l  36068  cdleme11  36069  cdleme14  36072  cdleme15a  36073  cdleme15c  36075  cdleme16b  36078  cdleme16c  36079  cdleme16d  36080  cdleme16e  36081  cdleme16f  36082  cdleme0nex  36089  cdleme18d  36094  cdleme19b  36103  cdleme19d  36105  cdleme19e  36106  cdleme20f  36113  cdleme20i  36116  cdleme20k  36118  cdleme20l1  36119  cdleme20l2  36120  cdleme20l  36121  cdleme20m  36122  cdleme21a  36124  cdleme21b  36125  cdleme21ct  36128  cdleme21d  36129  cdleme21e  36130  cdleme21f  36131  cdleme21h  36133  cdleme22eALTN  36144  cdleme22f2  36146  cdleme22g  36147  cdleme26e  36158  cdleme26eALTN  36160  cdleme26fALTN  36161  cdleme26f  36162  cdleme26f2ALTN  36163  cdleme26f2  36164  cdleme28a  36169  cdleme28b  36170  cdleme28  36172  cdleme29ex  36173  cdleme29c  36175  cdlemefrs29cpre1  36197  cdlemefr29exN  36201  cdlemefr32sn2aw  36203  cdlemefr29bpre0N  36205  cdlemefr29clN  36206  cdlemefr32fvaN  36208  cdlemefr32fva1  36209  cdlemefs32sn1aw  36213  cdleme43fsv1snlem  36219  cdleme41sn3a  36232  cdleme32fva  36236  cdleme32b  36241  cdleme32d  36243  cdleme32e  36244  cdleme32f  36245  cdleme32le  36246  cdleme35a  36247  cdleme35fnpq  36248  cdleme35b  36249  cdleme35c  36250  cdleme35d  36251  cdleme35e  36252  cdleme35f  36253  cdleme36a  36259  cdleme36m  36260  cdleme37m  36261  cdleme39a  36264  cdleme39n  36265  cdleme40m  36266  cdleme40n  36267  cdleme42e  36278  cdleme42f  36279  cdleme42g  36280  cdleme43bN  36289  cdleme43cN  36290  cdleme43dN  36291  cdleme46f2g2  36292  cdleme46f2g1  36293  cdleme17d2  36294  cdleme48b  36302  cdleme4gfv  36306  cdlemeg49le  36310  cdlemeg46c  36312  cdlemeg46fvaw  36315  cdlemeg46nlpq  36316  cdlemeg46frv  36324  cdlemeg46rgv  36327  cdlemeg46req  36328  cdlemeg46gfre  36331  cdleme50trn1  36348  cdleme50trn2a  36349  cdleme50trn2  36350  cdleme  36359  cdlemf  36362  trlord  36368  cdlemg2ce  36391  cdlemg7fvbwN  36406  cdlemg7aN  36424  cdlemg10bALTN  36435  cdlemg10a  36439  cdlemg10  36440  cdlemg12d  36445  cdlemg12f  36447  cdlemg12g  36448  cdlemg12  36449  cdlemg13a  36450  cdlemg13  36451  cdlemg17b  36461  cdlemg17dN  36462  cdlemg17dALTN  36463  cdlemg17e  36464  cdlemg17f  36465  cdlemg17g  36466  cdlemg17h  36467  cdlemg17i  36468  cdlemg17pq  36471  cdlemg17bq  36472  cdlemg17iqN  36473  cdlemg17  36476  cdlemg18d  36480  cdlemg18  36481  cdlemg19a  36482  cdlemg19  36483  cdlemg21  36485  cdlemg27a  36491  cdlemg28a  36492  cdlemg31b0N  36493  cdlemg27b  36495  cdlemg33b0  36500  cdlemg28b  36502  cdlemg28  36503  cdlemg33a  36505  cdlemg33  36510  cdlemg34  36511  cdlemg35  36512  cdlemg36  36513  ltrnco  36518  trlcone  36527  cdlemg44  36532  cdlemg47  36535  cdlemg48  36536  tendococl  36571  tendoplcl  36580  cdlemh1  36614  cdlemi  36619  cdlemj1  36620  cdlemj2  36621  tendocan  36623  cdlemk6  36636  cdlemki  36640  cdlemksat  36645  cdlemksv2  36646  cdlemk7  36647  cdlemk11  36648  cdlemk12  36649  cdlemkoatnle  36650  cdlemkole  36652  cdlemk14  36653  cdlemk15  36654  cdlemk16a  36655  cdlemk16  36656  cdlemk17  36657  cdlemk1u  36658  cdlemk5u  36660  cdlemk6u  36661  cdlemkuat  36665  cdlemk18  36667  cdlemk19  36668  cdlemk12u  36671  cdlemk21N  36672  cdlemk20  36673  cdlemkoatnle-2N  36674  cdlemk13-2N  36675  cdlemkole-2N  36676  cdlemk14-2N  36677  cdlemk15-2N  36678  cdlemk16-2N  36679  cdlemk17-2N  36680  cdlemk18-2N  36685  cdlemk19-2N  36686  cdlemk7u-2N  36687  cdlemk11u-2N  36688  cdlemk12u-2N  36689  cdlemk21-2N  36690  cdlemk20-2N  36691  cdlemk22  36692  cdlemk23-3  36701  cdlemk25-3  36703  cdlemk26b-3  36704  cdlemk27-3  36706  cdlemk28-3  36707  cdlemk33N  36708  cdlemk37  36713  cdlemky  36725  cdlemk11ta  36728  cdlemkid3N  36732  cdlemk11tc  36744  cdlemk11t  36745  cdlemk45  36746  cdlemk46  36747  cdlemk47  36748  cdlemk48  36749  cdlemk49  36750  cdlemk50  36751  cdlemk51  36752  cdlemk52  36753  cdlemk55b  36759  cdlemkyyN  36761  cdlemk55u1  36764  cdlemk55u  36765  cdlemk39u1  36766  cdlemk39u  36767  cdlemk56  36770  cdleml3N  36777  cdleml4N  36778  cdlemm10N  36917  dihord1  37017  dihord2a  37018  dihord2b  37019  dihord10  37022  dihord11c  37023  dihord2pre  37024  dihord4  37057  dihord5apre  37061  dihmeetlem1N  37089  dihglbcpreN  37099  dihjatc1  37110  dihjatc3  37112  dihmeetlem13N  37118  dihmeetlem20N  37125  baerlem3lem2  37509  baerlem5alem2  37510  baerlem5blem2  37511  hdmap14lem11  37677  hdmap14lem12  37678  monotuz  38025  congmul  38053  congsub  38056  rpnnen3lem  38117  ntrclsiso  38883  ntrclskb  38885  ntrclsk3  38886  wessf1ornlem  39878  infleinf  40086  lincdifsn  42799
  Copyright terms: Public domain W3C validator