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

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

Proof of Theorem simp12
StepHypRef Expression
1 simp2 1061 . 2 ((𝜑𝜓𝜒) → 𝜓)
213ad2ant1 1081 1 (((𝜑𝜓𝜒) ∧ 𝜃𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1037
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 1039
This theorem is referenced by:  simpl12  1136  simpr12  1145  simp112  1190  simp212  1199  simp312  1208  dvdsgcd  15255  coprimeprodsq  15507  pythagtriplem4  15518  pythagtriplem13  15526  pythagtriplem14  15527  pythagtriplem16  15529  pythagtrip  15533  pceu  15545  mremre  16258  lsmpropd  18084  m2cpminvid  20552  decpmatid  20569  mply1topmatcllem  20602  cmpsublem  21196  isfil2  21654  cxple2a  24439  isosctr  24545  brbtwn2  25779  colinearalg  25784  ax5seg  25812  axcontlem4  25841  bayesth  30486  bnj1204  31065  bnj1279  31071  nolesgn2o  31808  nolesgn2ores  31809  nolt02o  31829  ofscom  32098  btwndiff  32118  ifscgr  32135  brofs2  32168  brifs2  32169  fscgr  32171  btwnconn1lem1  32178  btwnconn1lem2  32179  btwnconn1lem3  32180  btwnconn1lem4  32181  btwnconn1lem12  32189  seglecgr12im  32201  seglecgr12  32202  ivthALT  32314  islshpcv  34166  lkrshp  34218  lshpsmreu  34222  lshpkrlem5  34227  cvrval3  34525  4noncolr3  34565  4noncolr2  34566  4noncolr1  34567  athgt  34568  3dimlem2  34571  3dimlem3a  34572  3dimlem4a  34575  3dimlem4  34576  3dimlem4OLDN  34577  1cvratex  34585  hlatexch4  34593  ps-2b  34594  3atlem4  34598  llnnleat  34625  2atm  34639  ps-2c  34640  llnmlplnN  34651  lplnnlelln  34655  2atmat  34673  lvoli2  34693  lvolnlelln  34696  4atlem3b  34710  4atlem10  34718  4atlem11a  34719  4atlem11b  34720  4atlem12a  34722  lplncvrlvol2  34727  2lplnja  34731  dalemswapyz  34768  lneq2at  34890  2lnat  34896  cdlema1N  34903  cdlemb  34906  paddasslem15  34946  pmodlem1  34958  llnmod2i2  34975  llnexchb2lem  34980  dalawlem1  34983  dalawlem3  34985  dalawlem4  34986  dalawlem6  34988  dalawlem7  34989  dalawlem9  34991  dalawlem10  34992  dalawlem11  34993  dalawlem12  34994  dalawlem13  34995  dalawlem15  34997  osumcllem5N  35072  osumcllem6N  35073  osumcllem7N  35074  osumcllem9N  35076  osumcllem10N  35077  osumcllem11N  35078  pl42lem1N  35091  lhpmcvr5N  35139  lhp2atne  35146  lhp2at0ne  35148  4atexlempw  35161  4atexlemex6  35186  4atexlem7  35187  ldilco  35228  ltrneq  35261  trlval2  35276  trlnidat  35286  cdlemd7  35317  cdleme7aa  35355  cdleme7c  35358  cdleme7d  35359  cdleme7e  35360  cdleme7ga  35361  cdleme7  35362  cdleme11c  35374  cdleme11e  35376  cdleme11l  35382  cdleme11  35383  cdleme14  35386  cdleme15a  35387  cdleme15c  35389  cdleme16b  35392  cdleme16c  35393  cdleme16d  35394  cdleme16e  35395  cdleme16f  35396  cdleme0nex  35403  cdleme18d  35408  cdleme19b  35418  cdleme19d  35420  cdleme19e  35421  cdleme20f  35428  cdleme20k  35433  cdleme20l1  35434  cdleme20l2  35435  cdleme20l  35436  cdleme20m  35437  cdleme21a  35439  cdleme21b  35440  cdleme21ct  35443  cdleme21d  35444  cdleme21e  35445  cdleme21f  35446  cdleme21h  35448  cdleme21i  35449  cdleme22eALTN  35459  cdleme22f2  35461  cdleme22g  35462  cdleme24  35466  cdleme25a  35467  cdleme25c  35469  cdleme25dN  35470  cdleme26e  35473  cdleme26ee  35474  cdleme26eALTN  35475  cdleme27N  35483  cdleme28a  35484  cdleme28b  35485  cdleme28  35487  cdlemefr32sn2aw  35518  cdlemefs32sn1aw  35528  cdleme43fsv1snlem  35534  cdleme41sn3a  35547  cdleme32c  35557  cdleme32e  35559  cdleme32le  35561  cdleme35a  35562  cdleme35b  35564  cdleme35c  35565  cdleme35e  35567  cdleme35f  35568  cdleme36a  35574  cdleme36m  35575  cdleme39a  35579  cdleme40m  35581  cdleme40n  35582  cdleme43bN  35604  cdleme43dN  35606  cdleme46f2g2  35607  cdleme46f2g1  35608  cdleme17d2  35609  cdleme4gfv  35621  cdlemeg49le  35625  cdlemeg46c  35627  cdlemeg46fvaw  35630  cdlemeg46nlpq  35631  cdlemeg46gfre  35646  cdleme50trn2  35665  cdleme  35674  cdlemg2idN  35710  cdlemg7fvbwN  35721  cdlemg10bALTN  35750  cdlemg10a  35754  cdlemg12d  35760  cdlemg12g  35763  cdlemg12  35764  cdlemg13a  35765  cdlemg13  35766  cdlemg17b  35776  cdlemg17dN  35777  cdlemg17dALTN  35778  cdlemg17e  35779  cdlemg17f  35780  cdlemg17i  35783  cdlemg17pq  35786  cdlemg17bq  35787  cdlemg17iqN  35788  cdlemg18d  35795  cdlemg18  35796  cdlemg19a  35797  cdlemg19  35798  cdlemg21  35800  cdlemg27a  35806  cdlemg28a  35807  cdlemg31b0N  35808  cdlemg27b  35810  cdlemg31c  35813  cdlemg33b0  35815  cdlemg33c0  35816  cdlemg28  35818  cdlemg33a  35820  cdlemg33  35825  cdlemg36  35828  ltrnco  35833  cdlemg44  35847  cdlemg47  35850  tendococl  35886  tendoplcl  35895  cdlemh1  35929  cdlemh2  35930  cdlemh  35931  cdlemi  35934  tendocan  35938  cdlemk5  35950  cdlemk6  35951  cdlemk7  35962  cdlemk11  35963  cdlemk12  35964  cdlemkole  35967  cdlemk14  35968  cdlemk15  35969  cdlemk16a  35970  cdlemk16  35971  cdlemk18  35982  cdlemk19  35983  cdlemk7u  35984  cdlemk11u  35985  cdlemk12u  35986  cdlemk21N  35987  cdlemk20  35988  cdlemkoatnle-2N  35989  cdlemk13-2N  35990  cdlemkole-2N  35991  cdlemk14-2N  35992  cdlemk15-2N  35993  cdlemk16-2N  35994  cdlemk17-2N  35995  cdlemk18-2N  36000  cdlemk19-2N  36001  cdlemk7u-2N  36002  cdlemk11u-2N  36003  cdlemk12u-2N  36004  cdlemk21-2N  36005  cdlemk20-2N  36006  cdlemk22  36007  cdlemk27-3  36021  cdlemk33N  36023  cdlemk11ta  36043  cdlemkid3N  36047  cdlemk11tc  36059  cdlemk11t  36060  cdlemk45  36061  cdlemk46  36062  cdlemk47  36063  cdlemk48  36064  cdlemk49  36065  cdlemk50  36066  cdlemk51  36067  cdlemk52  36068  cdlemk53a  36069  cdlemk55b  36074  cdlemkyyN  36076  cdlemk55u1  36079  cdlemk39u1  36081  cdlemk56  36085  cdlemm10N  36233  dihord1  36333  dihord2a  36334  dihord2b  36335  dihord10  36338  dihord4  36373  dihord5apre  36377  dihglblem2N  36409  dihjatc1  36426  dihjatc2N  36427  dihjatc3  36428  dihmeetlem15N  36436  dihmeetlem20N  36441  mapdpglem24  36819  hdmap14lem11  36996  hdmap14lem12  36997  mzpsubst  37137  monotuz  37332  congmul  37360  congsub  37363  ntrclsiso  38191  ntrclskb  38193  ntrclsk3  38194  infleinf  39407  mullimc  39654  mullimcf  39661  0ellimcdiv  39687  limclner  39689  sge0xaddlem2  40420  lincdifsn  41984
  Copyright terms: Public domain W3C validator