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

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

Proof of Theorem simp11
StepHypRef Expression
1 simp1 1059 . 2 ((𝜑𝜓𝜒) → 𝜑)
213ad2ant1 1080 1 (((𝜑𝜓𝜒) ∧ 𝜃𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  simpl11  1134  simpr11  1143  simp111  1188  simp211  1197  simp311  1206  funcnvqpOLD  5911  omeulem1  7607  omeu  7610  ackbij1lem16  9001  coprimeprodsq  15437  pythagtriplem14  15457  pythagtrip  15463  mrelatglb  17105  subglsm  18007  lsmpropd  18011  mdetmul  20348  decpmatid  20494  isfil2  21570  filuni  21599  cxple2a  24345  isosctr  24451  brbtwn2  25685  colinearalg  25690  ax5seglem3  25711  numclwwlkovf2ex  27075  measres  30066  bayesth  30282  ofscom  31756  btwndiff  31776  ifscgr  31793  brofs2  31826  brifs2  31827  fscgr  31829  btwnconn1lem1  31836  btwnconn1lem2  31837  btwnconn1lem3  31838  btwnconn1lem4  31839  btwnconn1lem5  31840  btwnconn1lem6  31841  btwnconn1lem7  31842  btwnconn1lem8  31843  btwnconn1lem9  31844  btwnconn1lem10  31845  btwnconn1lem11  31846  btwnconn1lem12  31847  seglecgr12im  31859  seglecgr12  31860  ivthALT  31972  eqlkr  33866  lkrshp  33872  lshpkrlem5  33881  cvrval3  34179  4noncolr3  34219  4noncolr2  34220  4noncolr1  34221  athgt  34222  3dimlem2  34225  3dimlem3a  34226  3dimlem4a  34229  3dimlem4  34230  3dimlem4OLDN  34231  3dim2  34234  1cvratex  34239  hlatexch4  34247  ps-2b  34248  3atlem1  34249  3atlem2  34250  3atlem4  34252  3atlem5  34253  3atlem6  34254  llnnleat  34279  2atm  34293  ps-2c  34294  llnmlplnN  34305  lplnnlelln  34309  2atmat  34327  2llnjN  34333  lvoli2  34347  lvolnlelln  34350  4atlem3b  34364  4atlem9  34369  4atlem10a  34370  4atlem10  34372  4atlem11a  34373  4atlem11b  34374  4atlem12a  34376  4atlem12b  34377  4at  34379  4at2  34380  lplncvrlvol2  34381  2lplnj  34386  dalemswapyz  34422  dath2  34503  lneq2at  34544  2lnat  34550  cdlema1N  34557  cdlemb  34560  paddasslem15  34600  pmodlem1  34612  llnmod2i2  34629  llnexchb2lem  34634  llnexchb2  34635  dalawlem1  34637  dalawlem3  34639  dalawlem4  34640  dalawlem5  34641  dalawlem6  34642  dalawlem7  34643  dalawlem8  34644  dalawlem9  34645  dalawlem10  34646  dalawlem11  34647  dalawlem12  34648  dalawlem13  34649  dalawlem15  34651  dalaw  34652  osumcllem5N  34726  osumcllem6N  34727  osumcllem7N  34728  osumcllem9N  34730  osumcllem10N  34731  osumcllem11N  34732  pl42lem1N  34745  lhpexle3lem  34777  lhpmcvr5N  34793  lhp2atne  34800  lhp2at0ne  34802  4atexlemswapqr  34829  4atexlemex6  34840  ldilco  34882  ltrneq  34915  trlval2  34930  trlnidat  34940  cdlemd2  34966  cdlemd7  34971  cdlemd8  34972  cdleme7aa  35009  cdleme7c  35012  cdleme7d  35013  cdleme7e  35014  cdleme7ga  35015  cdleme7  35016  cdleme11c  35028  cdleme11e  35030  cdleme11l  35036  cdleme11  35037  cdleme14  35040  cdleme15a  35041  cdleme15c  35043  cdleme16b  35046  cdleme16c  35047  cdleme16d  35048  cdleme16e  35049  cdleme16f  35050  cdleme0nex  35057  cdleme18d  35062  cdleme19b  35072  cdleme19d  35074  cdleme19e  35075  cdleme20f  35082  cdleme20i  35085  cdleme20k  35087  cdleme20l1  35088  cdleme20l2  35089  cdleme20l  35090  cdleme20m  35091  cdleme21a  35093  cdleme21b  35094  cdleme21ct  35097  cdleme21d  35098  cdleme21e  35099  cdleme21f  35100  cdleme21h  35102  cdleme22eALTN  35113  cdleme22f2  35115  cdleme22g  35116  cdleme26e  35127  cdleme26eALTN  35129  cdleme26fALTN  35130  cdleme26f  35131  cdleme26f2ALTN  35132  cdleme26f2  35133  cdleme28a  35138  cdleme28b  35139  cdleme28  35141  cdleme29ex  35142  cdleme29c  35144  cdlemefrs29cpre1  35166  cdlemefr29exN  35170  cdlemefr32sn2aw  35172  cdlemefr29bpre0N  35174  cdlemefr29clN  35175  cdlemefr32fvaN  35177  cdlemefr32fva1  35178  cdlemefs32sn1aw  35182  cdleme43fsv1snlem  35188  cdleme41sn3a  35201  cdleme32fva  35205  cdleme32b  35210  cdleme32d  35212  cdleme32e  35213  cdleme32f  35214  cdleme32le  35215  cdleme35a  35216  cdleme35fnpq  35217  cdleme35b  35218  cdleme35c  35219  cdleme35d  35220  cdleme35e  35221  cdleme35f  35222  cdleme36a  35228  cdleme36m  35229  cdleme37m  35230  cdleme39a  35233  cdleme39n  35234  cdleme40m  35235  cdleme40n  35236  cdleme42e  35247  cdleme42f  35248  cdleme42g  35249  cdleme43bN  35258  cdleme43cN  35259  cdleme43dN  35260  cdleme46f2g2  35261  cdleme46f2g1  35262  cdleme17d2  35263  cdleme48b  35271  cdleme4gfv  35275  cdlemeg49le  35279  cdlemeg46c  35281  cdlemeg46fvaw  35284  cdlemeg46nlpq  35285  cdlemeg46frv  35293  cdlemeg46rgv  35296  cdlemeg46req  35297  cdlemeg46gfre  35300  cdleme50trn1  35317  cdleme50trn2a  35318  cdleme50trn2  35319  cdleme  35328  cdlemf  35331  trlord  35337  cdlemg2ce  35360  cdlemg7fvbwN  35375  cdlemg7aN  35393  cdlemg10bALTN  35404  cdlemg10a  35408  cdlemg10  35409  cdlemg12d  35414  cdlemg12f  35416  cdlemg12g  35417  cdlemg12  35418  cdlemg13a  35419  cdlemg13  35420  cdlemg17b  35430  cdlemg17dN  35431  cdlemg17dALTN  35432  cdlemg17e  35433  cdlemg17f  35434  cdlemg17g  35435  cdlemg17h  35436  cdlemg17i  35437  cdlemg17pq  35440  cdlemg17bq  35441  cdlemg17iqN  35442  cdlemg17  35445  cdlemg18d  35449  cdlemg18  35450  cdlemg19a  35451  cdlemg19  35452  cdlemg21  35454  cdlemg27a  35460  cdlemg28a  35461  cdlemg31b0N  35462  cdlemg27b  35464  cdlemg33b0  35469  cdlemg28b  35471  cdlemg28  35472  cdlemg33a  35474  cdlemg33  35479  cdlemg34  35480  cdlemg35  35481  cdlemg36  35482  ltrnco  35487  trlcone  35496  cdlemg44  35501  cdlemg47  35504  cdlemg48  35505  tendococl  35540  tendoplcl  35549  cdlemh1  35583  cdlemi  35588  cdlemj1  35589  cdlemj2  35590  tendocan  35592  cdlemk6  35605  cdlemki  35609  cdlemksat  35614  cdlemksv2  35615  cdlemk7  35616  cdlemk11  35617  cdlemk12  35618  cdlemkoatnle  35619  cdlemkole  35621  cdlemk14  35622  cdlemk15  35623  cdlemk16a  35624  cdlemk16  35625  cdlemk17  35626  cdlemk1u  35627  cdlemk5u  35629  cdlemk6u  35630  cdlemkuat  35634  cdlemk18  35636  cdlemk19  35637  cdlemk12u  35640  cdlemk21N  35641  cdlemk20  35642  cdlemkoatnle-2N  35643  cdlemk13-2N  35644  cdlemkole-2N  35645  cdlemk14-2N  35646  cdlemk15-2N  35647  cdlemk16-2N  35648  cdlemk17-2N  35649  cdlemk18-2N  35654  cdlemk19-2N  35655  cdlemk7u-2N  35656  cdlemk11u-2N  35657  cdlemk12u-2N  35658  cdlemk21-2N  35659  cdlemk20-2N  35660  cdlemk22  35661  cdlemk23-3  35670  cdlemk25-3  35672  cdlemk26b-3  35673  cdlemk27-3  35675  cdlemk28-3  35676  cdlemk33N  35677  cdlemk37  35682  cdlemky  35694  cdlemk11ta  35697  cdlemkid3N  35701  cdlemk11tc  35713  cdlemk11t  35714  cdlemk45  35715  cdlemk46  35716  cdlemk47  35717  cdlemk48  35718  cdlemk49  35719  cdlemk50  35720  cdlemk51  35721  cdlemk52  35722  cdlemk55b  35728  cdlemkyyN  35730  cdlemk55u1  35733  cdlemk55u  35734  cdlemk39u1  35735  cdlemk39u  35736  cdlemk56  35739  cdleml3N  35746  cdleml4N  35747  cdlemm10N  35887  dihord1  35987  dihord2a  35988  dihord2b  35989  dihord10  35992  dihord11c  35993  dihord2pre  35994  dihord4  36027  dihord5apre  36031  dihmeetlem1N  36059  dihglbcpreN  36069  dihjatc1  36080  dihjatc3  36082  dihmeetlem13N  36088  dihmeetlem20N  36095  baerlem3lem2  36479  baerlem5alem2  36480  baerlem5blem2  36481  hdmap14lem11  36650  hdmap14lem12  36651  monotuz  36986  congmul  37014  congsub  37017  rpnnen3lem  37078  ntrclsiso  37847  ntrclskb  37849  ntrclsk3  37850  wessf1ornlem  38845  infleinf  39052  lincdifsn  41501
  Copyright terms: Public domain W3C validator