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

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

Proof of Theorem simp12
StepHypRef Expression
1 simp2 1082 . 2 ((𝜑𝜓𝜒) → 𝜓)
213ad2ant1 1102 1 (((𝜑𝜓𝜒) ∧ 𝜃𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1054
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 1056
This theorem is referenced by:  simpl12  1157  simpr12  1166  simp112  1211  simp212  1220  simp312  1229  dvdsgcd  15308  coprimeprodsq  15560  pythagtriplem4  15571  pythagtriplem13  15579  pythagtriplem14  15580  pythagtriplem16  15582  pythagtrip  15586  pceu  15598  mremre  16311  lsmpropd  18136  m2cpminvid  20606  decpmatid  20623  mply1topmatcllem  20656  cmpsublem  21250  isfil2  21707  cxple2a  24490  isosctr  24596  brbtwn2  25830  colinearalg  25835  ax5seg  25863  axcontlem4  25892  bayesth  30629  bnj1204  31206  bnj1279  31212  nolesgn2o  31949  nolesgn2ores  31950  nolt02o  31970  ofscom  32239  btwndiff  32259  ifscgr  32276  brofs2  32309  brifs2  32310  fscgr  32312  btwnconn1lem1  32319  btwnconn1lem2  32320  btwnconn1lem3  32321  btwnconn1lem4  32322  btwnconn1lem12  32330  seglecgr12im  32342  seglecgr12  32343  ivthALT  32455  islshpcv  34658  lkrshp  34710  lshpsmreu  34714  lshpkrlem5  34719  cvrval3  35017  4noncolr3  35057  4noncolr2  35058  4noncolr1  35059  athgt  35060  3dimlem2  35063  3dimlem3a  35064  3dimlem4a  35067  3dimlem4  35068  3dimlem4OLDN  35069  1cvratex  35077  hlatexch4  35085  ps-2b  35086  3atlem4  35090  llnnleat  35117  2atm  35131  ps-2c  35132  llnmlplnN  35143  lplnnlelln  35147  2atmat  35165  lvoli2  35185  lvolnlelln  35188  4atlem3b  35202  4atlem10  35210  4atlem11a  35211  4atlem11b  35212  4atlem12a  35214  lplncvrlvol2  35219  2lplnja  35223  dalemswapyz  35260  lneq2at  35382  2lnat  35388  cdlema1N  35395  cdlemb  35398  paddasslem15  35438  pmodlem1  35450  llnmod2i2  35467  llnexchb2lem  35472  dalawlem1  35475  dalawlem3  35477  dalawlem4  35478  dalawlem6  35480  dalawlem7  35481  dalawlem9  35483  dalawlem10  35484  dalawlem11  35485  dalawlem12  35486  dalawlem13  35487  dalawlem15  35489  osumcllem5N  35564  osumcllem6N  35565  osumcllem7N  35566  osumcllem9N  35568  osumcllem10N  35569  osumcllem11N  35570  pl42lem1N  35583  lhpmcvr5N  35631  lhp2atne  35638  lhp2at0ne  35640  4atexlempw  35653  4atexlemex6  35678  4atexlem7  35679  ldilco  35720  ltrneq  35753  trlval2  35768  trlnidat  35778  cdlemd7  35809  cdleme7aa  35847  cdleme7c  35850  cdleme7d  35851  cdleme7e  35852  cdleme7ga  35853  cdleme7  35854  cdleme11c  35866  cdleme11e  35868  cdleme11l  35874  cdleme11  35875  cdleme14  35878  cdleme15a  35879  cdleme15c  35881  cdleme16b  35884  cdleme16c  35885  cdleme16d  35886  cdleme16e  35887  cdleme16f  35888  cdleme0nex  35895  cdleme18d  35900  cdleme19b  35909  cdleme19d  35911  cdleme19e  35912  cdleme20f  35919  cdleme20k  35924  cdleme20l1  35925  cdleme20l2  35926  cdleme20l  35927  cdleme20m  35928  cdleme21a  35930  cdleme21b  35931  cdleme21ct  35934  cdleme21d  35935  cdleme21e  35936  cdleme21f  35937  cdleme21h  35939  cdleme21i  35940  cdleme22eALTN  35950  cdleme22f2  35952  cdleme22g  35953  cdleme24  35957  cdleme25a  35958  cdleme25c  35960  cdleme25dN  35961  cdleme26e  35964  cdleme26ee  35965  cdleme26eALTN  35966  cdleme27N  35974  cdleme28a  35975  cdleme28b  35976  cdleme28  35978  cdlemefr32sn2aw  36009  cdlemefs32sn1aw  36019  cdleme43fsv1snlem  36025  cdleme41sn3a  36038  cdleme32c  36048  cdleme32e  36050  cdleme32le  36052  cdleme35a  36053  cdleme35b  36055  cdleme35c  36056  cdleme35e  36058  cdleme35f  36059  cdleme36a  36065  cdleme36m  36066  cdleme39a  36070  cdleme40m  36072  cdleme40n  36073  cdleme43bN  36095  cdleme43dN  36097  cdleme46f2g2  36098  cdleme46f2g1  36099  cdleme17d2  36100  cdleme4gfv  36112  cdlemeg49le  36116  cdlemeg46c  36118  cdlemeg46fvaw  36121  cdlemeg46nlpq  36122  cdlemeg46gfre  36137  cdleme50trn2  36156  cdleme  36165  cdlemg2idN  36201  cdlemg7fvbwN  36212  cdlemg10bALTN  36241  cdlemg10a  36245  cdlemg12d  36251  cdlemg12g  36254  cdlemg12  36255  cdlemg13a  36256  cdlemg13  36257  cdlemg17b  36267  cdlemg17dN  36268  cdlemg17dALTN  36269  cdlemg17e  36270  cdlemg17f  36271  cdlemg17i  36274  cdlemg17pq  36277  cdlemg17bq  36278  cdlemg17iqN  36279  cdlemg18d  36286  cdlemg18  36287  cdlemg19a  36288  cdlemg19  36289  cdlemg21  36291  cdlemg27a  36297  cdlemg28a  36298  cdlemg31b0N  36299  cdlemg27b  36301  cdlemg31c  36304  cdlemg33b0  36306  cdlemg33c0  36307  cdlemg28  36309  cdlemg33a  36311  cdlemg33  36316  cdlemg36  36319  ltrnco  36324  cdlemg44  36338  cdlemg47  36341  tendococl  36377  tendoplcl  36386  cdlemh1  36420  cdlemh2  36421  cdlemh  36422  cdlemi  36425  tendocan  36429  cdlemk5  36441  cdlemk6  36442  cdlemk7  36453  cdlemk11  36454  cdlemk12  36455  cdlemkole  36458  cdlemk14  36459  cdlemk15  36460  cdlemk16a  36461  cdlemk16  36462  cdlemk18  36473  cdlemk19  36474  cdlemk7u  36475  cdlemk11u  36476  cdlemk12u  36477  cdlemk21N  36478  cdlemk20  36479  cdlemkoatnle-2N  36480  cdlemk13-2N  36481  cdlemkole-2N  36482  cdlemk14-2N  36483  cdlemk15-2N  36484  cdlemk16-2N  36485  cdlemk17-2N  36486  cdlemk18-2N  36491  cdlemk19-2N  36492  cdlemk7u-2N  36493  cdlemk11u-2N  36494  cdlemk12u-2N  36495  cdlemk21-2N  36496  cdlemk20-2N  36497  cdlemk22  36498  cdlemk27-3  36512  cdlemk33N  36514  cdlemk11ta  36534  cdlemkid3N  36538  cdlemk11tc  36550  cdlemk11t  36551  cdlemk45  36552  cdlemk46  36553  cdlemk47  36554  cdlemk48  36555  cdlemk49  36556  cdlemk50  36557  cdlemk51  36558  cdlemk52  36559  cdlemk53a  36560  cdlemk55b  36565  cdlemkyyN  36567  cdlemk55u1  36570  cdlemk39u1  36572  cdlemk56  36576  cdlemm10N  36724  dihord1  36824  dihord2a  36825  dihord2b  36826  dihord10  36829  dihord4  36864  dihord5apre  36868  dihglblem2N  36900  dihjatc1  36917  dihjatc2N  36918  dihjatc3  36919  dihmeetlem15N  36927  dihmeetlem20N  36932  mapdpglem24  37310  hdmap14lem11  37487  hdmap14lem12  37488  mzpsubst  37628  monotuz  37823  congmul  37851  congsub  37854  ntrclsiso  38682  ntrclskb  38684  ntrclsk3  38685  infleinf  39901  mullimc  40166  mullimcf  40173  0ellimcdiv  40199  limclner  40201  sge0xaddlem2  40969  lincdifsn  42538
  Copyright terms: Public domain W3C validator