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

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

Proof of Theorem simp11
StepHypRef Expression
1 simp1 1131 . 2 ((𝜑𝜓𝜒) → 𝜑)
213ad2ant1 1128 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:  simpl11OLD  1316  simpr11OLD  1334  simp111  1387  simp211  1396  simp311  1405  funcnvqpOLD  6114  omeulem1  7831  omeu  7834  ackbij1lem16  9249  coprimeprodsq  15715  pythagtriplem14  15735  pythagtrip  15741  mrelatglb  17385  subglsm  18286  lsmpropd  18290  mdetmul  20631  decpmatid  20777  isfil2  21861  filuni  21890  cxple2a  24644  isosctr  24750  brbtwn2  25984  colinearalg  25989  ax5seglem3  26010  clwwlknonex2  27258  measres  30594  bayesth  30810  nolesgn2o  32130  nolesgn2ores  32131  nolt02o  32151  ofscom  32420  btwndiff  32440  ifscgr  32457  brofs2  32490  brifs2  32491  fscgr  32493  btwnconn1lem1  32500  btwnconn1lem2  32501  btwnconn1lem3  32502  btwnconn1lem4  32503  btwnconn1lem5  32504  btwnconn1lem6  32505  btwnconn1lem7  32506  btwnconn1lem8  32507  btwnconn1lem9  32508  btwnconn1lem10  32509  btwnconn1lem11  32510  btwnconn1lem12  32511  seglecgr12im  32523  seglecgr12  32524  ivthALT  32636  eqlkr  34889  lkrshp  34895  lshpkrlem5  34904  cvrval3  35202  4noncolr3  35242  4noncolr2  35243  4noncolr1  35244  athgt  35245  3dimlem2  35248  3dimlem3a  35249  3dimlem4a  35252  3dimlem4  35253  3dimlem4OLDN  35254  3dim2  35257  1cvratex  35262  hlatexch4  35270  ps-2b  35271  3atlem1  35272  3atlem2  35273  3atlem4  35275  3atlem5  35276  3atlem6  35277  llnnleat  35302  2atm  35316  ps-2c  35317  llnmlplnN  35328  lplnnlelln  35332  2atmat  35350  2llnjN  35356  lvoli2  35370  lvolnlelln  35373  4atlem3b  35387  4atlem9  35392  4atlem10a  35393  4atlem10  35395  4atlem11a  35396  4atlem11b  35397  4atlem12a  35399  4atlem12b  35400  4at  35402  4at2  35403  lplncvrlvol2  35404  2lplnj  35409  dalemswapyz  35445  dath2  35526  lneq2at  35567  2lnat  35573  cdlema1N  35580  cdlemb  35583  paddasslem15  35623  pmodlem1  35635  llnmod2i2  35652  llnexchb2lem  35657  llnexchb2  35658  dalawlem1  35660  dalawlem3  35662  dalawlem4  35663  dalawlem5  35664  dalawlem6  35665  dalawlem7  35666  dalawlem8  35667  dalawlem9  35668  dalawlem10  35669  dalawlem11  35670  dalawlem12  35671  dalawlem13  35672  dalawlem15  35674  dalaw  35675  osumcllem5N  35749  osumcllem6N  35750  osumcllem7N  35751  osumcllem9N  35753  osumcllem10N  35754  osumcllem11N  35755  pl42lem1N  35768  lhpexle3lem  35800  lhpmcvr5N  35816  lhp2atne  35823  lhp2at0ne  35825  4atexlemswapqr  35852  4atexlemex6  35863  ldilco  35905  ltrneq  35938  trlval2  35953  trlnidat  35963  cdlemd2  35989  cdlemd7  35994  cdlemd8  35995  cdleme7aa  36032  cdleme7c  36035  cdleme7d  36036  cdleme7e  36037  cdleme7ga  36038  cdleme7  36039  cdleme11c  36051  cdleme11e  36053  cdleme11l  36059  cdleme11  36060  cdleme14  36063  cdleme15a  36064  cdleme15c  36066  cdleme16b  36069  cdleme16c  36070  cdleme16d  36071  cdleme16e  36072  cdleme16f  36073  cdleme0nex  36080  cdleme18d  36085  cdleme19b  36094  cdleme19d  36096  cdleme19e  36097  cdleme20f  36104  cdleme20i  36107  cdleme20k  36109  cdleme20l1  36110  cdleme20l2  36111  cdleme20l  36112  cdleme20m  36113  cdleme21a  36115  cdleme21b  36116  cdleme21ct  36119  cdleme21d  36120  cdleme21e  36121  cdleme21f  36122  cdleme21h  36124  cdleme22eALTN  36135  cdleme22f2  36137  cdleme22g  36138  cdleme26e  36149  cdleme26eALTN  36151  cdleme26fALTN  36152  cdleme26f  36153  cdleme26f2ALTN  36154  cdleme26f2  36155  cdleme28a  36160  cdleme28b  36161  cdleme28  36163  cdleme29ex  36164  cdleme29c  36166  cdlemefrs29cpre1  36188  cdlemefr29exN  36192  cdlemefr32sn2aw  36194  cdlemefr29bpre0N  36196  cdlemefr29clN  36197  cdlemefr32fvaN  36199  cdlemefr32fva1  36200  cdlemefs32sn1aw  36204  cdleme43fsv1snlem  36210  cdleme41sn3a  36223  cdleme32fva  36227  cdleme32b  36232  cdleme32d  36234  cdleme32e  36235  cdleme32f  36236  cdleme32le  36237  cdleme35a  36238  cdleme35fnpq  36239  cdleme35b  36240  cdleme35c  36241  cdleme35d  36242  cdleme35e  36243  cdleme35f  36244  cdleme36a  36250  cdleme36m  36251  cdleme37m  36252  cdleme39a  36255  cdleme39n  36256  cdleme40m  36257  cdleme40n  36258  cdleme42e  36269  cdleme42f  36270  cdleme42g  36271  cdleme43bN  36280  cdleme43cN  36281  cdleme43dN  36282  cdleme46f2g2  36283  cdleme46f2g1  36284  cdleme17d2  36285  cdleme48b  36293  cdleme4gfv  36297  cdlemeg49le  36301  cdlemeg46c  36303  cdlemeg46fvaw  36306  cdlemeg46nlpq  36307  cdlemeg46frv  36315  cdlemeg46rgv  36318  cdlemeg46req  36319  cdlemeg46gfre  36322  cdleme50trn1  36339  cdleme50trn2a  36340  cdleme50trn2  36341  cdleme  36350  cdlemf  36353  trlord  36359  cdlemg2ce  36382  cdlemg7fvbwN  36397  cdlemg7aN  36415  cdlemg10bALTN  36426  cdlemg10a  36430  cdlemg10  36431  cdlemg12d  36436  cdlemg12f  36438  cdlemg12g  36439  cdlemg12  36440  cdlemg13a  36441  cdlemg13  36442  cdlemg17b  36452  cdlemg17dN  36453  cdlemg17dALTN  36454  cdlemg17e  36455  cdlemg17f  36456  cdlemg17g  36457  cdlemg17h  36458  cdlemg17i  36459  cdlemg17pq  36462  cdlemg17bq  36463  cdlemg17iqN  36464  cdlemg17  36467  cdlemg18d  36471  cdlemg18  36472  cdlemg19a  36473  cdlemg19  36474  cdlemg21  36476  cdlemg27a  36482  cdlemg28a  36483  cdlemg31b0N  36484  cdlemg27b  36486  cdlemg33b0  36491  cdlemg28b  36493  cdlemg28  36494  cdlemg33a  36496  cdlemg33  36501  cdlemg34  36502  cdlemg35  36503  cdlemg36  36504  ltrnco  36509  trlcone  36518  cdlemg44  36523  cdlemg47  36526  cdlemg48  36527  tendococl  36562  tendoplcl  36571  cdlemh1  36605  cdlemi  36610  cdlemj1  36611  cdlemj2  36612  tendocan  36614  cdlemk6  36627  cdlemki  36631  cdlemksat  36636  cdlemksv2  36637  cdlemk7  36638  cdlemk11  36639  cdlemk12  36640  cdlemkoatnle  36641  cdlemkole  36643  cdlemk14  36644  cdlemk15  36645  cdlemk16a  36646  cdlemk16  36647  cdlemk17  36648  cdlemk1u  36649  cdlemk5u  36651  cdlemk6u  36652  cdlemkuat  36656  cdlemk18  36658  cdlemk19  36659  cdlemk12u  36662  cdlemk21N  36663  cdlemk20  36664  cdlemkoatnle-2N  36665  cdlemk13-2N  36666  cdlemkole-2N  36667  cdlemk14-2N  36668  cdlemk15-2N  36669  cdlemk16-2N  36670  cdlemk17-2N  36671  cdlemk18-2N  36676  cdlemk19-2N  36677  cdlemk7u-2N  36678  cdlemk11u-2N  36679  cdlemk12u-2N  36680  cdlemk21-2N  36681  cdlemk20-2N  36682  cdlemk22  36683  cdlemk23-3  36692  cdlemk25-3  36694  cdlemk26b-3  36695  cdlemk27-3  36697  cdlemk28-3  36698  cdlemk33N  36699  cdlemk37  36704  cdlemky  36716  cdlemk11ta  36719  cdlemkid3N  36723  cdlemk11tc  36735  cdlemk11t  36736  cdlemk45  36737  cdlemk46  36738  cdlemk47  36739  cdlemk48  36740  cdlemk49  36741  cdlemk50  36742  cdlemk51  36743  cdlemk52  36744  cdlemk55b  36750  cdlemkyyN  36752  cdlemk55u1  36755  cdlemk55u  36756  cdlemk39u1  36757  cdlemk39u  36758  cdlemk56  36761  cdleml3N  36768  cdleml4N  36769  cdlemm10N  36909  dihord1  37009  dihord2a  37010  dihord2b  37011  dihord10  37014  dihord11c  37015  dihord2pre  37016  dihord4  37049  dihord5apre  37053  dihmeetlem1N  37081  dihglbcpreN  37091  dihjatc1  37102  dihjatc3  37104  dihmeetlem13N  37110  dihmeetlem20N  37117  baerlem3lem2  37501  baerlem5alem2  37502  baerlem5blem2  37503  hdmap14lem11  37672  hdmap14lem12  37673  monotuz  38008  congmul  38036  congsub  38039  rpnnen3lem  38100  ntrclsiso  38867  ntrclskb  38869  ntrclsk3  38870  wessf1ornlem  39870  infleinf  40086  lincdifsn  42723
  Copyright terms: Public domain W3C validator