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

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

Proof of Theorem simp13
StepHypRef Expression
1 simp3 1133 . 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:  simpl13OLD  1320  simpr13OLD  1338  simp113  1389  simp213  1398  simp313  1407  funtpgOLD  6104  omeu  7834  ackbij1lem16  9249  dvdsgcd  15463  coprimeprodsq  15715  pythagtriplem4  15726  pythagtriplem13  15734  pythagtriplem14  15735  pythagtriplem16  15737  pythagtrip  15741  lsmpropd  18290  matsc  20458  mdetunilem7  20626  smadiadetglem2  20680  m2cpminvid  20760  pmatcollpw1lem1  20781  mp2pm2mplem2  20814  isfil2  21861  filuni  21890  ufprim  21914  cxple2a  24644  isosctr  24750  brbtwn2  25984  colinearalg  25989  ax5seg  26017  axcontlem4  26046  measres  30594  bayesth  30810  nolesgn2o  32130  ofscom  32420  btwndiff  32440  ifscgr  32457  brofs2  32490  brifs2  32491  fscgr  32493  btwnconn1lem1  32500  btwnconn1lem2  32501  btwnconn1lem3  32502  btwnconn1lem4  32503  btwnconn1lem12  32511  seglecgr12im  32523  seglecgr12  32524  ivthALT  32636  islshpcv  34843  eqlkr  34889  lshpsmreu  34899  lshpkrlem5  34904  atlrelat1  35111  cvlcvr1  35129  cvlcvrp  35130  cvlatcvr1  35131  cvlatcvr2  35132  4noncolr3  35242  4noncolr2  35243  4noncolr1  35244  athgt  35245  3dimlem2  35248  3dimlem3a  35249  3dimlem4a  35252  3dimlem4  35253  3dimlem4OLDN  35254  3dim1  35256  3dim2  35257  hlatexch4  35270  ps-2b  35271  3atlem6  35277  llnnleat  35302  2atm  35316  ps-2c  35317  llnmlplnN  35328  2atmat  35350  2llnjN  35356  lvoli2  35370  4atlem3b  35387  4atlem10  35395  4atlem11a  35396  4atlem11b  35397  4atlem12a  35399  4atlem12b  35400  dalemswapyz  35445  lneq2at  35567  2lnat  35573  cdlema1N  35580  cdlemb  35583  pmodlem1  35635  llnmod2i2  35652  dalawlem1  35660  dalawlem3  35662  dalawlem4  35663  dalawlem6  35665  dalawlem9  35668  dalawlem10  35669  dalawlem11  35670  dalawlem12  35671  dalawlem13  35672  dalawlem15  35674  dalaw  35675  pclfinN  35689  osumcllem5N  35749  osumcllem6N  35750  osumcllem7N  35751  osumcllem9N  35753  osumcllem11N  35755  pl42lem1N  35768  lhp2at0  35821  lhp2atne  35823  lhp2at0ne  35825  4atexlem7  35864  ldilco  35905  ltrneq  35938  cdlemd2  35989  cdleme0ex2N  36014  cdleme7aa  36032  cdleme7c  36035  cdleme7d  36036  cdleme7ga  36038  cdleme11c  36051  cdleme11l  36059  cdleme11  36060  cdleme14  36063  cdleme15a  36064  cdleme15c  36066  cdleme16b  36069  cdleme16c  36070  cdleme16d  36071  cdleme16e  36072  cdleme16f  36073  cdleme0nex  36080  cdleme19b  36094  cdleme19d  36096  cdleme19e  36097  cdleme20f  36104  cdleme20k  36109  cdleme20l1  36110  cdleme20l2  36111  cdleme20l  36112  cdleme20m  36113  cdleme21a  36115  cdleme21b  36116  cdleme21c  36117  cdleme21ct  36119  cdleme21d  36120  cdleme21e  36121  cdleme21f  36122  cdleme21i  36125  cdleme22cN  36132  cdleme22eALTN  36135  cdleme25a  36143  cdleme25c  36145  cdleme25dN  36146  cdleme26e  36149  cdleme26ee  36150  cdleme26eALTN  36151  cdleme26f2ALTN  36154  cdleme26f2  36155  cdleme28a  36160  cdleme28b  36161  cdleme28  36163  cdlemefr32sn2aw  36194  cdlemefs32sn1aw  36204  cdleme43fsv1snlem  36210  cdleme41sn3a  36223  cdleme32c  36233  cdleme32e  36235  cdleme32le  36237  cdleme35a  36238  cdleme35b  36240  cdleme35d  36242  cdleme36a  36250  cdleme36m  36251  cdleme39a  36255  cdleme40m  36257  cdleme40n  36258  cdleme43bN  36280  cdleme43dN  36282  cdleme46f2g2  36283  cdleme46f2g1  36284  cdleme4gfv  36297  cdlemeg49le  36301  cdlemeg46c  36303  cdlemeg46fvaw  36306  cdlemeg46nlpq  36307  cdlemeg46gfre  36322  cdleme50trn2  36341  cdlemg2ce  36382  cdlemg2idN  36386  cdlemg7fvbwN  36397  cdlemg10bALTN  36426  cdlemg10a  36430  cdlemg12d  36436  cdlemg12g  36439  cdlemg12  36440  cdlemg13a  36441  cdlemg13  36442  cdlemg17b  36452  cdlemg17dN  36453  cdlemg17dALTN  36454  cdlemg17e  36455  cdlemg17pq  36462  cdlemg17bq  36463  cdlemg18d  36471  cdlemg19a  36473  cdlemg19  36474  cdlemg21  36476  cdlemg27a  36482  cdlemg31b0N  36484  cdlemg27b  36486  cdlemg31c  36489  cdlemg33b0  36491  cdlemg33c0  36492  cdlemg28b  36493  cdlemg33a  36496  cdlemg33  36501  ltrnco  36509  cdlemg44  36523  cdlemg47  36526  tendococl  36562  tendoplcl  36571  cdlemh1  36605  cdlemh2  36606  cdlemh  36607  cdlemi  36610  cdlemk5  36626  cdlemk6  36627  cdlemksel  36635  cdlemksv2  36637  cdlemk7  36638  cdlemk11  36639  cdlemk12  36640  cdlemkole  36643  cdlemk14  36644  cdlemk15  36645  cdlemk16a  36646  cdlemk16  36647  cdlemk1u  36649  cdlemk5u  36651  cdlemk6u  36652  cdlemkuel  36655  cdlemkuv2  36657  cdlemk18  36658  cdlemk19  36659  cdlemk7u  36660  cdlemk11u  36661  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  cdlemkuel-3  36688  cdlemkuv2-3N  36689  cdlemk22-3  36691  cdlemk33N  36699  cdlemk47  36739  cdlemk48  36740  cdlemk49  36741  cdlemk50  36742  cdlemk51  36743  cdlemk52  36744  cdlemk53a  36745  cdlemk55b  36750  cdlemkyyN  36752  cdlemk55u1  36755  cdlemk39u1  36757  cdlemk56  36761  dihord1  37009  dihord2a  37010  dihord10  37014  dihord11c  37015  dihord4  37049  dihord5apre  37053  dihglblem2N  37085  dihglbcpreN  37091  dihmeetlem3N  37096  dihjatc1  37102  dihjatc2N  37103  dihjatc3  37104  mapdpglem24  37495  baerlem3lem2  37501  baerlem5alem2  37502  baerlem5blem2  37503  hdmap14lem11  37672  hdmap14lem12  37673  hdmapglem7  37723  mzpsubst  37813  congmul  38036  congsub  38039  ntrclsiso  38867  ntrclskb  38869  ntrclsk3  38870  limsupre  40376  0ellimcdiv  40384  limclner  40386  sge0xaddlem2  41154  lincdifsn  42723
  Copyright terms: Public domain W3C validator