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

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

Proof of Theorem simp13
StepHypRef Expression
1 simp3 1168 . 2 ((𝜑𝜓𝜒) → 𝜒)
213ad2ant1 1163 1 (((𝜑𝜓𝜒) ∧ 𝜃𝜏) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1107
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 198  df-an 385  df-3an 1109
This theorem is referenced by:  simpl13OLD  1334  simpr13OLD  1352  simp113  1403  simp213  1412  simp313  1421  omeu  7870  ackbij1lem16  9310  dvdsgcd  15542  coprimeprodsq  15792  pythagtriplem4  15803  pythagtriplem13  15811  pythagtriplem14  15812  pythagtriplem16  15814  pythagtrip  15818  lsmpropd  18354  matsc  20533  mdetunilem7  20701  smadiadetglem2  20756  m2cpminvid  20837  pmatcollpw1lem1  20858  mp2pm2mplem2  20891  isfil2  21939  filuni  21968  ufprim  21992  cxple2a  24736  isosctr  24842  brbtwn2  26076  colinearalg  26081  ax5seg  26109  axcontlem4  26138  measres  30732  bayesth  30949  nolesgn2o  32268  ofscom  32558  btwndiff  32578  ifscgr  32595  brofs2  32628  brifs2  32629  fscgr  32631  btwnconn1lem1  32638  btwnconn1lem2  32639  btwnconn1lem3  32640  btwnconn1lem4  32641  btwnconn1lem12  32649  seglecgr12im  32661  seglecgr12  32662  ivthALT  32773  islshpcv  35009  eqlkr  35055  lshpsmreu  35065  lshpkrlem5  35070  atlrelat1  35277  cvlcvr1  35295  cvlcvrp  35296  cvlatcvr1  35297  cvlatcvr2  35298  4noncolr3  35409  4noncolr2  35410  4noncolr1  35411  athgt  35412  3dimlem2  35415  3dimlem3a  35416  3dimlem4a  35419  3dimlem4  35420  3dimlem4OLDN  35421  3dim1  35423  3dim2  35424  hlatexch4  35437  ps-2b  35438  3atlem6  35444  llnnleat  35469  2atm  35483  ps-2c  35484  llnmlplnN  35495  2atmat  35517  2llnjN  35523  lvoli2  35537  4atlem3b  35554  4atlem10  35562  4atlem11a  35563  4atlem11b  35564  4atlem12a  35566  4atlem12b  35567  dalemswapyz  35612  lneq2at  35734  2lnat  35740  cdlema1N  35747  cdlemb  35750  pmodlem1  35802  llnmod2i2  35819  dalawlem1  35827  dalawlem3  35829  dalawlem4  35830  dalawlem6  35832  dalawlem9  35835  dalawlem10  35836  dalawlem11  35837  dalawlem12  35838  dalawlem13  35839  dalawlem15  35841  dalaw  35842  pclfinN  35856  osumcllem5N  35916  osumcllem6N  35917  osumcllem7N  35918  osumcllem9N  35920  osumcllem11N  35922  pl42lem1N  35935  lhp2at0  35988  lhp2atne  35990  lhp2at0ne  35992  4atexlem7  36031  ldilco  36072  ltrneq  36105  cdlemd2  36155  cdleme0ex2N  36180  cdleme7aa  36198  cdleme7c  36201  cdleme7d  36202  cdleme7ga  36204  cdleme11c  36217  cdleme11l  36225  cdleme11  36226  cdleme14  36229  cdleme15a  36230  cdleme15c  36232  cdleme16b  36235  cdleme16c  36236  cdleme16d  36237  cdleme16e  36238  cdleme16f  36239  cdleme0nex  36246  cdleme19b  36260  cdleme19d  36262  cdleme19e  36263  cdleme20f  36270  cdleme20k  36275  cdleme20l1  36276  cdleme20l2  36277  cdleme20l  36278  cdleme20m  36279  cdleme21a  36281  cdleme21b  36282  cdleme21c  36283  cdleme21ct  36285  cdleme21d  36286  cdleme21e  36287  cdleme21f  36288  cdleme21i  36291  cdleme22cN  36298  cdleme22eALTN  36301  cdleme25a  36309  cdleme25c  36311  cdleme25dN  36312  cdleme26e  36315  cdleme26ee  36316  cdleme26eALTN  36317  cdleme26f2ALTN  36320  cdleme26f2  36321  cdleme28a  36326  cdleme28b  36327  cdleme28  36329  cdlemefr32sn2aw  36360  cdlemefs32sn1aw  36370  cdleme43fsv1snlem  36376  cdleme41sn3a  36389  cdleme32c  36399  cdleme32e  36401  cdleme32le  36403  cdleme35a  36404  cdleme35b  36406  cdleme35d  36408  cdleme36a  36416  cdleme36m  36417  cdleme39a  36421  cdleme40m  36423  cdleme40n  36424  cdleme43bN  36446  cdleme43dN  36448  cdleme46f2g2  36449  cdleme46f2g1  36450  cdleme4gfv  36463  cdlemeg49le  36467  cdlemeg46c  36469  cdlemeg46fvaw  36472  cdlemeg46nlpq  36473  cdlemeg46gfre  36488  cdleme50trn2  36507  cdlemg2ce  36548  cdlemg2idN  36552  cdlemg7fvbwN  36563  cdlemg10bALTN  36592  cdlemg10a  36596  cdlemg12d  36602  cdlemg12g  36605  cdlemg12  36606  cdlemg13a  36607  cdlemg13  36608  cdlemg17b  36618  cdlemg17dN  36619  cdlemg17dALTN  36620  cdlemg17e  36621  cdlemg17pq  36628  cdlemg17bq  36629  cdlemg18d  36637  cdlemg19a  36639  cdlemg19  36640  cdlemg21  36642  cdlemg27a  36648  cdlemg31b0N  36650  cdlemg27b  36652  cdlemg31c  36655  cdlemg33b0  36657  cdlemg33c0  36658  cdlemg28b  36659  cdlemg33a  36662  cdlemg33  36667  ltrnco  36675  cdlemg44  36689  cdlemg47  36692  tendococl  36728  tendoplcl  36737  cdlemh1  36771  cdlemh2  36772  cdlemh  36773  cdlemi  36776  cdlemk5  36792  cdlemk6  36793  cdlemksel  36801  cdlemksv2  36803  cdlemk7  36804  cdlemk11  36805  cdlemk12  36806  cdlemkole  36809  cdlemk14  36810  cdlemk15  36811  cdlemk16a  36812  cdlemk16  36813  cdlemk1u  36815  cdlemk5u  36817  cdlemk6u  36818  cdlemkuel  36821  cdlemkuv2  36823  cdlemk18  36824  cdlemk19  36825  cdlemk7u  36826  cdlemk11u  36827  cdlemk12u  36828  cdlemk21N  36829  cdlemk20  36830  cdlemkoatnle-2N  36831  cdlemk13-2N  36832  cdlemkole-2N  36833  cdlemk14-2N  36834  cdlemk15-2N  36835  cdlemk16-2N  36836  cdlemk17-2N  36837  cdlemk18-2N  36842  cdlemk19-2N  36843  cdlemk7u-2N  36844  cdlemk11u-2N  36845  cdlemk12u-2N  36846  cdlemk21-2N  36847  cdlemk20-2N  36848  cdlemkuel-3  36854  cdlemkuv2-3N  36855  cdlemk22-3  36857  cdlemk33N  36865  cdlemk47  36905  cdlemk48  36906  cdlemk49  36907  cdlemk50  36908  cdlemk51  36909  cdlemk52  36910  cdlemk53a  36911  cdlemk55b  36916  cdlemkyyN  36918  cdlemk55u1  36921  cdlemk39u1  36923  cdlemk56  36927  dihord1  37174  dihord2a  37175  dihord10  37179  dihord11c  37180  dihord4  37214  dihord5apre  37218  dihglblem2N  37250  dihglbcpreN  37256  dihmeetlem3N  37261  dihjatc1  37267  dihjatc2N  37268  dihjatc3  37269  mapdpglem24  37660  baerlem3lem2  37666  baerlem5alem2  37667  baerlem5blem2  37668  hdmap14lem11  37834  hdmap14lem12  37835  hdmapglem7  37885  mzpsubst  37989  congmul  38211  congsub  38214  ntrclsiso  39039  ntrclskb  39041  ntrclsk3  39042  limsupre  40511  0ellimcdiv  40519  limclner  40521  sge0xaddlem2  41288  lincdifsn  42882
  Copyright terms: Public domain W3C validator