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

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

Proof of Theorem simp13
StepHypRef Expression
1 simp3 1061 . 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:  simpl13  1136  simpr13  1145  simp113  1190  simp213  1199  simp313  1208  funtpgOLD  5901  omeu  7610  ackbij1lem16  9001  dvdsgcd  15185  coprimeprodsq  15437  pythagtriplem4  15448  pythagtriplem13  15456  pythagtriplem14  15457  pythagtriplem16  15459  pythagtrip  15463  lsmpropd  18011  matsc  20175  mdetunilem7  20343  smadiadetglem2  20397  m2cpminvid  20477  pmatcollpw1lem1  20498  mp2pm2mplem2  20531  isfil2  21570  filuni  21599  ufprim  21623  cxple2a  24345  isosctr  24451  brbtwn2  25685  colinearalg  25690  ax5seg  25718  axcontlem4  25747  measres  30066  bayesth  30282  ofscom  31756  btwndiff  31776  ifscgr  31793  brofs2  31826  brifs2  31827  fscgr  31829  btwnconn1lem1  31836  btwnconn1lem2  31837  btwnconn1lem3  31838  btwnconn1lem4  31839  btwnconn1lem12  31847  seglecgr12im  31859  seglecgr12  31860  ivthALT  31972  islshpcv  33820  eqlkr  33866  lshpsmreu  33876  lshpkrlem5  33881  atlrelat1  34088  cvlcvr1  34106  cvlcvrp  34107  cvlatcvr1  34108  cvlatcvr2  34109  4noncolr3  34219  4noncolr2  34220  4noncolr1  34221  athgt  34222  3dimlem2  34225  3dimlem3a  34226  3dimlem4a  34229  3dimlem4  34230  3dimlem4OLDN  34231  3dim1  34233  3dim2  34234  hlatexch4  34247  ps-2b  34248  3atlem6  34254  llnnleat  34279  2atm  34293  ps-2c  34294  llnmlplnN  34305  2atmat  34327  2llnjN  34333  lvoli2  34347  4atlem3b  34364  4atlem10  34372  4atlem11a  34373  4atlem11b  34374  4atlem12a  34376  4atlem12b  34377  dalemswapyz  34422  lneq2at  34544  2lnat  34550  cdlema1N  34557  cdlemb  34560  pmodlem1  34612  llnmod2i2  34629  dalawlem1  34637  dalawlem3  34639  dalawlem4  34640  dalawlem6  34642  dalawlem9  34645  dalawlem10  34646  dalawlem11  34647  dalawlem12  34648  dalawlem13  34649  dalawlem15  34651  dalaw  34652  pclfinN  34666  osumcllem5N  34726  osumcllem6N  34727  osumcllem7N  34728  osumcllem9N  34730  osumcllem11N  34732  pl42lem1N  34745  lhp2at0  34798  lhp2atne  34800  lhp2at0ne  34802  4atexlem7  34841  ldilco  34882  ltrneq  34915  cdlemd2  34966  cdleme0ex2N  34991  cdleme7aa  35009  cdleme7c  35012  cdleme7d  35013  cdleme7ga  35015  cdleme11c  35028  cdleme11l  35036  cdleme11  35037  cdleme14  35040  cdleme15a  35041  cdleme15c  35043  cdleme16b  35046  cdleme16c  35047  cdleme16d  35048  cdleme16e  35049  cdleme16f  35050  cdleme0nex  35057  cdleme19b  35072  cdleme19d  35074  cdleme19e  35075  cdleme20f  35082  cdleme20k  35087  cdleme20l1  35088  cdleme20l2  35089  cdleme20l  35090  cdleme20m  35091  cdleme21a  35093  cdleme21b  35094  cdleme21c  35095  cdleme21ct  35097  cdleme21d  35098  cdleme21e  35099  cdleme21f  35100  cdleme21i  35103  cdleme22cN  35110  cdleme22eALTN  35113  cdleme25a  35121  cdleme25c  35123  cdleme25dN  35124  cdleme26e  35127  cdleme26ee  35128  cdleme26eALTN  35129  cdleme26f2ALTN  35132  cdleme26f2  35133  cdleme28a  35138  cdleme28b  35139  cdleme28  35141  cdlemefr32sn2aw  35172  cdlemefs32sn1aw  35182  cdleme43fsv1snlem  35188  cdleme41sn3a  35201  cdleme32c  35211  cdleme32e  35213  cdleme32le  35215  cdleme35a  35216  cdleme35b  35218  cdleme35d  35220  cdleme36a  35228  cdleme36m  35229  cdleme39a  35233  cdleme40m  35235  cdleme40n  35236  cdleme43bN  35258  cdleme43dN  35260  cdleme46f2g2  35261  cdleme46f2g1  35262  cdleme4gfv  35275  cdlemeg49le  35279  cdlemeg46c  35281  cdlemeg46fvaw  35284  cdlemeg46nlpq  35285  cdlemeg46gfre  35300  cdleme50trn2  35319  cdlemg2ce  35360  cdlemg2idN  35364  cdlemg7fvbwN  35375  cdlemg10bALTN  35404  cdlemg10a  35408  cdlemg12d  35414  cdlemg12g  35417  cdlemg12  35418  cdlemg13a  35419  cdlemg13  35420  cdlemg17b  35430  cdlemg17dN  35431  cdlemg17dALTN  35432  cdlemg17e  35433  cdlemg17pq  35440  cdlemg17bq  35441  cdlemg18d  35449  cdlemg19a  35451  cdlemg19  35452  cdlemg21  35454  cdlemg27a  35460  cdlemg31b0N  35462  cdlemg27b  35464  cdlemg31c  35467  cdlemg33b0  35469  cdlemg33c0  35470  cdlemg28b  35471  cdlemg33a  35474  cdlemg33  35479  ltrnco  35487  cdlemg44  35501  cdlemg47  35504  tendococl  35540  tendoplcl  35549  cdlemh1  35583  cdlemh2  35584  cdlemh  35585  cdlemi  35588  cdlemk5  35604  cdlemk6  35605  cdlemksel  35613  cdlemksv2  35615  cdlemk7  35616  cdlemk11  35617  cdlemk12  35618  cdlemkole  35621  cdlemk14  35622  cdlemk15  35623  cdlemk16a  35624  cdlemk16  35625  cdlemk1u  35627  cdlemk5u  35629  cdlemk6u  35630  cdlemkuel  35633  cdlemkuv2  35635  cdlemk18  35636  cdlemk19  35637  cdlemk7u  35638  cdlemk11u  35639  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  cdlemkuel-3  35666  cdlemkuv2-3N  35667  cdlemk22-3  35669  cdlemk33N  35677  cdlemk47  35717  cdlemk48  35718  cdlemk49  35719  cdlemk50  35720  cdlemk51  35721  cdlemk52  35722  cdlemk53a  35723  cdlemk55b  35728  cdlemkyyN  35730  cdlemk55u1  35733  cdlemk39u1  35735  cdlemk56  35739  dihord1  35987  dihord2a  35988  dihord10  35992  dihord11c  35993  dihord4  36027  dihord5apre  36031  dihglblem2N  36063  dihglbcpreN  36069  dihmeetlem3N  36074  dihjatc1  36080  dihjatc2N  36081  dihjatc3  36082  mapdpglem24  36473  baerlem3lem2  36479  baerlem5alem2  36480  baerlem5blem2  36481  hdmap14lem11  36650  hdmap14lem12  36651  hdmapglem7  36701  mzpsubst  36791  congmul  37014  congsub  37017  ntrclsiso  37847  ntrclskb  37849  ntrclsk3  37850  limsupre  39277  0ellimcdiv  39285  limclner  39287  sge0xaddlem2  39958  lincdifsn  41501
  Copyright terms: Public domain W3C validator