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

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

Proof of Theorem simp11
StepHypRef Expression
1 simp1 1133 . 2 ((𝜑𝜓𝜒) → 𝜑)
213ad2ant1 1130 1 (((𝜑𝜓𝜒) ∧ 𝜃𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  simp111  1299  simp211  1308  simp311  1317  omeulem1  8195  omeu  8198  ackbij1lem16  9650  coprimeprodsq  16139  pythagtriplem14  16159  pythagtrip  16165  mrelatglb  17790  subglsm  18795  lsmpropd  18799  mdetmul  21232  decpmatid  21379  isfil2  22465  filuni  22494  cxple2a  25294  isosctr  25411  brbtwn2  26703  colinearalg  26708  ax5seglem3  26729  clwwlknonex2  27898  measres  31595  bayesth  31811  nolesgn2o  33292  nolesgn2ores  33293  nolt02o  33313  ofscom  33582  btwndiff  33602  ifscgr  33619  brofs2  33652  brifs2  33653  fscgr  33655  btwnconn1lem1  33662  btwnconn1lem2  33663  btwnconn1lem3  33664  btwnconn1lem4  33665  btwnconn1lem5  33666  btwnconn1lem6  33667  btwnconn1lem7  33668  btwnconn1lem8  33669  btwnconn1lem9  33670  btwnconn1lem10  33671  btwnconn1lem11  33672  btwnconn1lem12  33673  seglecgr12im  33685  seglecgr12  33686  ivthALT  33797  eqlkr  36394  lkrshp  36400  lshpkrlem5  36409  cvrval3  36708  4noncolr3  36748  4noncolr2  36749  4noncolr1  36750  athgt  36751  3dimlem2  36754  3dimlem3a  36755  3dimlem4a  36758  3dimlem4  36759  3dimlem4OLDN  36760  3dim2  36763  1cvratex  36768  hlatexch4  36776  ps-2b  36777  3atlem1  36778  3atlem2  36779  3atlem4  36781  3atlem5  36782  3atlem6  36783  llnnleat  36808  2atm  36822  ps-2c  36823  llnmlplnN  36834  lplnnlelln  36838  2atmat  36856  2llnjN  36862  lvoli2  36876  lvolnlelln  36879  4atlem3b  36893  4atlem9  36898  4atlem10a  36899  4atlem10  36901  4atlem11a  36902  4atlem11b  36903  4atlem12a  36905  4atlem12b  36906  4at  36908  4at2  36909  lplncvrlvol2  36910  2lplnj  36915  dalemswapyz  36951  dath2  37032  lneq2at  37073  2lnat  37079  cdlema1N  37086  cdlemb  37089  paddasslem15  37129  pmodlem1  37141  llnmod2i2  37158  llnexchb2lem  37163  llnexchb2  37164  dalawlem1  37166  dalawlem3  37168  dalawlem4  37169  dalawlem5  37170  dalawlem6  37171  dalawlem7  37172  dalawlem8  37173  dalawlem9  37174  dalawlem10  37175  dalawlem11  37176  dalawlem12  37177  dalawlem13  37178  dalawlem15  37180  dalaw  37181  osumcllem5N  37255  osumcllem6N  37256  osumcllem7N  37257  osumcllem9N  37259  osumcllem10N  37260  osumcllem11N  37261  pl42lem1N  37274  lhpexle3lem  37306  lhpmcvr5N  37322  lhp2atne  37329  lhp2at0ne  37331  4atexlemswapqr  37358  4atexlemex6  37369  ldilco  37411  ltrneq  37444  trlval2  37458  trlnidat  37468  cdlemd2  37494  cdlemd7  37499  cdlemd8  37500  cdleme7aa  37537  cdleme7c  37540  cdleme7d  37541  cdleme7e  37542  cdleme7ga  37543  cdleme7  37544  cdleme11c  37556  cdleme11e  37558  cdleme11l  37564  cdleme11  37565  cdleme14  37568  cdleme15a  37569  cdleme15c  37571  cdleme16b  37574  cdleme16c  37575  cdleme16d  37576  cdleme16e  37577  cdleme16f  37578  cdleme0nex  37585  cdleme18d  37590  cdleme19b  37599  cdleme19d  37601  cdleme19e  37602  cdleme20f  37609  cdleme20i  37612  cdleme20k  37614  cdleme20l1  37615  cdleme20l2  37616  cdleme20l  37617  cdleme20m  37618  cdleme21a  37620  cdleme21b  37621  cdleme21ct  37624  cdleme21d  37625  cdleme21e  37626  cdleme21f  37627  cdleme21h  37629  cdleme22eALTN  37640  cdleme22f2  37642  cdleme22g  37643  cdleme26e  37654  cdleme26eALTN  37656  cdleme26fALTN  37657  cdleme26f  37658  cdleme26f2ALTN  37659  cdleme26f2  37660  cdleme28a  37665  cdleme28b  37666  cdleme28  37668  cdleme29ex  37669  cdleme29c  37671  cdlemefrs29cpre1  37693  cdlemefr29exN  37697  cdlemefr32sn2aw  37699  cdlemefr29bpre0N  37701  cdlemefr29clN  37702  cdlemefr32fvaN  37704  cdlemefr32fva1  37705  cdlemefs32sn1aw  37709  cdleme43fsv1snlem  37715  cdleme41sn3a  37728  cdleme32fva  37732  cdleme32b  37737  cdleme32d  37739  cdleme32e  37740  cdleme32f  37741  cdleme32le  37742  cdleme35a  37743  cdleme35fnpq  37744  cdleme35b  37745  cdleme35c  37746  cdleme35d  37747  cdleme35e  37748  cdleme35f  37749  cdleme36a  37755  cdleme36m  37756  cdleme37m  37757  cdleme39a  37760  cdleme39n  37761  cdleme40m  37762  cdleme40n  37763  cdleme42e  37774  cdleme42f  37775  cdleme42g  37776  cdleme43bN  37785  cdleme43cN  37786  cdleme43dN  37787  cdleme46f2g2  37788  cdleme46f2g1  37789  cdleme17d2  37790  cdleme48b  37798  cdleme4gfv  37802  cdlemeg49le  37806  cdlemeg46c  37808  cdlemeg46fvaw  37811  cdlemeg46nlpq  37812  cdlemeg46frv  37820  cdlemeg46rgv  37823  cdlemeg46req  37824  cdlemeg46gfre  37827  cdleme50trn1  37844  cdleme50trn2a  37845  cdleme50trn2  37846  cdleme  37855  cdlemf  37858  trlord  37864  cdlemg2ce  37887  cdlemg7fvbwN  37902  cdlemg7aN  37920  cdlemg10bALTN  37931  cdlemg10a  37935  cdlemg10  37936  cdlemg12d  37941  cdlemg12f  37943  cdlemg12g  37944  cdlemg12  37945  cdlemg13a  37946  cdlemg13  37947  cdlemg17b  37957  cdlemg17dN  37958  cdlemg17dALTN  37959  cdlemg17e  37960  cdlemg17f  37961  cdlemg17g  37962  cdlemg17h  37963  cdlemg17i  37964  cdlemg17pq  37967  cdlemg17bq  37968  cdlemg17iqN  37969  cdlemg17  37972  cdlemg18d  37976  cdlemg18  37977  cdlemg19a  37978  cdlemg19  37979  cdlemg21  37981  cdlemg27a  37987  cdlemg28a  37988  cdlemg31b0N  37989  cdlemg27b  37991  cdlemg33b0  37996  cdlemg28b  37998  cdlemg28  37999  cdlemg33a  38001  cdlemg33  38006  cdlemg34  38007  cdlemg35  38008  cdlemg36  38009  ltrnco  38014  trlcone  38023  cdlemg44  38028  cdlemg47  38031  cdlemg48  38032  tendococl  38067  tendoplcl  38076  cdlemh1  38110  cdlemi  38115  cdlemj1  38116  cdlemj2  38117  tendocan  38119  cdlemk6  38132  cdlemki  38136  cdlemksat  38141  cdlemksv2  38142  cdlemk7  38143  cdlemk11  38144  cdlemk12  38145  cdlemkoatnle  38146  cdlemkole  38148  cdlemk14  38149  cdlemk15  38150  cdlemk16a  38151  cdlemk16  38152  cdlemk17  38153  cdlemk1u  38154  cdlemk5u  38156  cdlemk6u  38157  cdlemkuat  38161  cdlemk18  38163  cdlemk19  38164  cdlemk12u  38167  cdlemk21N  38168  cdlemk20  38169  cdlemkoatnle-2N  38170  cdlemk13-2N  38171  cdlemkole-2N  38172  cdlemk14-2N  38173  cdlemk15-2N  38174  cdlemk16-2N  38175  cdlemk17-2N  38176  cdlemk18-2N  38181  cdlemk19-2N  38182  cdlemk7u-2N  38183  cdlemk11u-2N  38184  cdlemk12u-2N  38185  cdlemk21-2N  38186  cdlemk20-2N  38187  cdlemk22  38188  cdlemk23-3  38197  cdlemk25-3  38199  cdlemk26b-3  38200  cdlemk27-3  38202  cdlemk28-3  38203  cdlemk33N  38204  cdlemk37  38209  cdlemky  38221  cdlemk11ta  38224  cdlemkid3N  38228  cdlemk11tc  38240  cdlemk11t  38241  cdlemk45  38242  cdlemk46  38243  cdlemk47  38244  cdlemk48  38245  cdlemk49  38246  cdlemk50  38247  cdlemk51  38248  cdlemk52  38249  cdlemk55b  38255  cdlemkyyN  38257  cdlemk55u1  38260  cdlemk55u  38261  cdlemk39u1  38262  cdlemk39u  38263  cdlemk56  38266  cdleml3N  38273  cdleml4N  38274  cdlemm10N  38413  dihord1  38513  dihord2a  38514  dihord2b  38515  dihord10  38518  dihord11c  38519  dihord2pre  38520  dihord4  38553  dihord5apre  38557  dihmeetlem1N  38585  dihglbcpreN  38595  dihjatc1  38606  dihjatc3  38608  dihmeetlem13N  38614  dihmeetlem20N  38621  baerlem3lem2  39005  baerlem5alem2  39006  baerlem5blem2  39007  hdmap14lem11  39173  hdmap14lem12  39174  monotuz  39875  congmul  39901  congsub  39904  rpnnen3lem  39965  ntrclsiso  40763  ntrclskb  40765  ntrclsk3  40766  wessf1ornlem  41804  infleinf  41997  lincdifsn  44826  itsclc0yqe  45168  itsclc0xyqsolr  45176
  Copyright terms: Public domain W3C validator