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

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

Proof of Theorem simp13
StepHypRef Expression
1 simp3 1130 . 2 ((𝜑𝜓𝜒) → 𝜒)
213ad2ant1 1125 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:  simpl13  1287  simpr13  1296  simp113  1341  simp213  1350  simp313  1359  funtpgOLD  6056  omeu  7785  ackbij1lem16  9170  dvdsgcd  15384  coprimeprodsq  15636  pythagtriplem4  15647  pythagtriplem13  15655  pythagtriplem14  15656  pythagtriplem16  15658  pythagtrip  15662  lsmpropd  18211  matsc  20379  mdetunilem7  20547  smadiadetglem2  20601  m2cpminvid  20681  pmatcollpw1lem1  20702  mp2pm2mplem2  20735  isfil2  21782  filuni  21811  ufprim  21835  cxple2a  24565  isosctr  24671  brbtwn2  25905  colinearalg  25910  ax5seg  25938  axcontlem4  25967  measres  30515  bayesth  30731  nolesgn2o  32051  ofscom  32341  btwndiff  32361  ifscgr  32378  brofs2  32411  brifs2  32412  fscgr  32414  btwnconn1lem1  32421  btwnconn1lem2  32422  btwnconn1lem3  32423  btwnconn1lem4  32424  btwnconn1lem12  32432  seglecgr12im  32444  seglecgr12  32445  ivthALT  32557  islshpcv  34760  eqlkr  34806  lshpsmreu  34816  lshpkrlem5  34821  atlrelat1  35028  cvlcvr1  35046  cvlcvrp  35047  cvlatcvr1  35048  cvlatcvr2  35049  4noncolr3  35159  4noncolr2  35160  4noncolr1  35161  athgt  35162  3dimlem2  35165  3dimlem3a  35166  3dimlem4a  35169  3dimlem4  35170  3dimlem4OLDN  35171  3dim1  35173  3dim2  35174  hlatexch4  35187  ps-2b  35188  3atlem6  35194  llnnleat  35219  2atm  35233  ps-2c  35234  llnmlplnN  35245  2atmat  35267  2llnjN  35273  lvoli2  35287  4atlem3b  35304  4atlem10  35312  4atlem11a  35313  4atlem11b  35314  4atlem12a  35316  4atlem12b  35317  dalemswapyz  35362  lneq2at  35484  2lnat  35490  cdlema1N  35497  cdlemb  35500  pmodlem1  35552  llnmod2i2  35569  dalawlem1  35577  dalawlem3  35579  dalawlem4  35580  dalawlem6  35582  dalawlem9  35585  dalawlem10  35586  dalawlem11  35587  dalawlem12  35588  dalawlem13  35589  dalawlem15  35591  dalaw  35592  pclfinN  35606  osumcllem5N  35666  osumcllem6N  35667  osumcllem7N  35668  osumcllem9N  35670  osumcllem11N  35672  pl42lem1N  35685  lhp2at0  35738  lhp2atne  35740  lhp2at0ne  35742  4atexlem7  35781  ldilco  35822  ltrneq  35855  cdlemd2  35906  cdleme0ex2N  35931  cdleme7aa  35949  cdleme7c  35952  cdleme7d  35953  cdleme7ga  35955  cdleme11c  35968  cdleme11l  35976  cdleme11  35977  cdleme14  35980  cdleme15a  35981  cdleme15c  35983  cdleme16b  35986  cdleme16c  35987  cdleme16d  35988  cdleme16e  35989  cdleme16f  35990  cdleme0nex  35997  cdleme19b  36011  cdleme19d  36013  cdleme19e  36014  cdleme20f  36021  cdleme20k  36026  cdleme20l1  36027  cdleme20l2  36028  cdleme20l  36029  cdleme20m  36030  cdleme21a  36032  cdleme21b  36033  cdleme21c  36034  cdleme21ct  36036  cdleme21d  36037  cdleme21e  36038  cdleme21f  36039  cdleme21i  36042  cdleme22cN  36049  cdleme22eALTN  36052  cdleme25a  36060  cdleme25c  36062  cdleme25dN  36063  cdleme26e  36066  cdleme26ee  36067  cdleme26eALTN  36068  cdleme26f2ALTN  36071  cdleme26f2  36072  cdleme28a  36077  cdleme28b  36078  cdleme28  36080  cdlemefr32sn2aw  36111  cdlemefs32sn1aw  36121  cdleme43fsv1snlem  36127  cdleme41sn3a  36140  cdleme32c  36150  cdleme32e  36152  cdleme32le  36154  cdleme35a  36155  cdleme35b  36157  cdleme35d  36159  cdleme36a  36167  cdleme36m  36168  cdleme39a  36172  cdleme40m  36174  cdleme40n  36175  cdleme43bN  36197  cdleme43dN  36199  cdleme46f2g2  36200  cdleme46f2g1  36201  cdleme4gfv  36214  cdlemeg49le  36218  cdlemeg46c  36220  cdlemeg46fvaw  36223  cdlemeg46nlpq  36224  cdlemeg46gfre  36239  cdleme50trn2  36258  cdlemg2ce  36299  cdlemg2idN  36303  cdlemg7fvbwN  36314  cdlemg10bALTN  36343  cdlemg10a  36347  cdlemg12d  36353  cdlemg12g  36356  cdlemg12  36357  cdlemg13a  36358  cdlemg13  36359  cdlemg17b  36369  cdlemg17dN  36370  cdlemg17dALTN  36371  cdlemg17e  36372  cdlemg17pq  36379  cdlemg17bq  36380  cdlemg18d  36388  cdlemg19a  36390  cdlemg19  36391  cdlemg21  36393  cdlemg27a  36399  cdlemg31b0N  36401  cdlemg27b  36403  cdlemg31c  36406  cdlemg33b0  36408  cdlemg33c0  36409  cdlemg28b  36410  cdlemg33a  36413  cdlemg33  36418  ltrnco  36426  cdlemg44  36440  cdlemg47  36443  tendococl  36479  tendoplcl  36488  cdlemh1  36522  cdlemh2  36523  cdlemh  36524  cdlemi  36527  cdlemk5  36543  cdlemk6  36544  cdlemksel  36552  cdlemksv2  36554  cdlemk7  36555  cdlemk11  36556  cdlemk12  36557  cdlemkole  36560  cdlemk14  36561  cdlemk15  36562  cdlemk16a  36563  cdlemk16  36564  cdlemk1u  36566  cdlemk5u  36568  cdlemk6u  36569  cdlemkuel  36572  cdlemkuv2  36574  cdlemk18  36575  cdlemk19  36576  cdlemk7u  36577  cdlemk11u  36578  cdlemk12u  36579  cdlemk21N  36580  cdlemk20  36581  cdlemkoatnle-2N  36582  cdlemk13-2N  36583  cdlemkole-2N  36584  cdlemk14-2N  36585  cdlemk15-2N  36586  cdlemk16-2N  36587  cdlemk17-2N  36588  cdlemk18-2N  36593  cdlemk19-2N  36594  cdlemk7u-2N  36595  cdlemk11u-2N  36596  cdlemk12u-2N  36597  cdlemk21-2N  36598  cdlemk20-2N  36599  cdlemkuel-3  36605  cdlemkuv2-3N  36606  cdlemk22-3  36608  cdlemk33N  36616  cdlemk47  36656  cdlemk48  36657  cdlemk49  36658  cdlemk50  36659  cdlemk51  36660  cdlemk52  36661  cdlemk53a  36662  cdlemk55b  36667  cdlemkyyN  36669  cdlemk55u1  36672  cdlemk39u1  36674  cdlemk56  36678  dihord1  36926  dihord2a  36927  dihord10  36931  dihord11c  36932  dihord4  36966  dihord5apre  36970  dihglblem2N  37002  dihglbcpreN  37008  dihmeetlem3N  37013  dihjatc1  37019  dihjatc2N  37020  dihjatc3  37021  mapdpglem24  37412  baerlem3lem2  37418  baerlem5alem2  37419  baerlem5blem2  37420  hdmap14lem11  37589  hdmap14lem12  37590  hdmapglem7  37640  mzpsubst  37730  congmul  37953  congsub  37956  ntrclsiso  38784  ntrclskb  38786  ntrclsk3  38787  limsupre  40293  0ellimcdiv  40301  limclner  40303  sge0xaddlem2  41071  lincdifsn  42640
  Copyright terms: Public domain W3C validator