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

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

Proof of Theorem simp12
StepHypRef Expression
1 simp2 1054 . 2 ((𝜑𝜓𝜒) → 𝜓)
213ad2ant1 1074 1 (((𝜑𝜓𝜒) ∧ 𝜃𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  simpl12  1129  simpr12  1138  simp112  1183  simp212  1192  simp312  1201  dvdsgcd  15042  coprimeprodsq  15294  pythagtriplem4  15305  pythagtriplem13  15313  pythagtriplem14  15314  pythagtriplem16  15316  pythagtrip  15320  pceu  15332  mremre  16030  lsmpropd  17856  m2cpminvid  20316  decpmatid  20333  mply1topmatcllem  20366  cmpsublem  20951  isfil2  21409  cxple2a  24159  isosctr  24265  brbtwn2  25500  colinearalg  25505  ax5seg  25533  axcontlem4  25562  bayesth  29631  bnj1204  30137  bnj1279  30143  ofscom  31087  btwndiff  31107  ifscgr  31124  brofs2  31157  brifs2  31158  fscgr  31160  btwnconn1lem1  31167  btwnconn1lem2  31168  btwnconn1lem3  31169  btwnconn1lem4  31170  btwnconn1lem12  31178  seglecgr12im  31190  seglecgr12  31191  ivthALT  31303  islshpcv  33158  lkrshp  33210  lshpsmreu  33214  lshpkrlem5  33219  cvrval3  33517  4noncolr3  33557  4noncolr2  33558  4noncolr1  33559  athgt  33560  3dimlem2  33563  3dimlem3a  33564  3dimlem4a  33567  3dimlem4  33568  3dimlem4OLDN  33569  1cvratex  33577  hlatexch4  33585  ps-2b  33586  3atlem4  33590  llnnleat  33617  2atm  33631  ps-2c  33632  llnmlplnN  33643  lplnnlelln  33647  2atmat  33665  lvoli2  33685  lvolnlelln  33688  4atlem3b  33702  4atlem10  33710  4atlem11a  33711  4atlem11b  33712  4atlem12a  33714  lplncvrlvol2  33719  2lplnja  33723  dalemswapyz  33760  lneq2at  33882  2lnat  33888  cdlema1N  33895  cdlemb  33898  paddasslem15  33938  pmodlem1  33950  llnmod2i2  33967  llnexchb2lem  33972  dalawlem1  33975  dalawlem3  33977  dalawlem4  33978  dalawlem6  33980  dalawlem7  33981  dalawlem9  33983  dalawlem10  33984  dalawlem11  33985  dalawlem12  33986  dalawlem13  33987  dalawlem15  33989  osumcllem5N  34064  osumcllem6N  34065  osumcllem7N  34066  osumcllem9N  34068  osumcllem10N  34069  osumcllem11N  34070  pl42lem1N  34083  lhpmcvr5N  34131  lhp2atne  34138  lhp2at0ne  34140  4atexlempw  34153  4atexlemex6  34178  4atexlem7  34179  ldilco  34220  ltrneq  34253  trlval2  34268  trlnidat  34278  cdlemd7  34309  cdleme7aa  34347  cdleme7c  34350  cdleme7d  34351  cdleme7e  34352  cdleme7ga  34353  cdleme7  34354  cdleme11c  34366  cdleme11e  34368  cdleme11l  34374  cdleme11  34375  cdleme14  34378  cdleme15a  34379  cdleme15c  34381  cdleme16b  34384  cdleme16c  34385  cdleme16d  34386  cdleme16e  34387  cdleme16f  34388  cdleme0nex  34395  cdleme18d  34400  cdleme19b  34410  cdleme19d  34412  cdleme19e  34413  cdleme20f  34420  cdleme20k  34425  cdleme20l1  34426  cdleme20l2  34427  cdleme20l  34428  cdleme20m  34429  cdleme21a  34431  cdleme21b  34432  cdleme21ct  34435  cdleme21d  34436  cdleme21e  34437  cdleme21f  34438  cdleme21h  34440  cdleme21i  34441  cdleme22eALTN  34451  cdleme22f2  34453  cdleme22g  34454  cdleme24  34458  cdleme25a  34459  cdleme25c  34461  cdleme25dN  34462  cdleme26e  34465  cdleme26ee  34466  cdleme26eALTN  34467  cdleme27N  34475  cdleme28a  34476  cdleme28b  34477  cdleme28  34479  cdlemefr32sn2aw  34510  cdlemefs32sn1aw  34520  cdleme43fsv1snlem  34526  cdleme41sn3a  34539  cdleme32c  34549  cdleme32e  34551  cdleme32le  34553  cdleme35a  34554  cdleme35b  34556  cdleme35c  34557  cdleme35e  34559  cdleme35f  34560  cdleme36a  34566  cdleme36m  34567  cdleme39a  34571  cdleme40m  34573  cdleme40n  34574  cdleme43bN  34596  cdleme43dN  34598  cdleme46f2g2  34599  cdleme46f2g1  34600  cdleme17d2  34601  cdleme4gfv  34613  cdlemeg49le  34617  cdlemeg46c  34619  cdlemeg46fvaw  34622  cdlemeg46nlpq  34623  cdlemeg46gfre  34638  cdleme50trn2  34657  cdleme  34666  cdlemg2idN  34702  cdlemg7fvbwN  34713  cdlemg10bALTN  34742  cdlemg10a  34746  cdlemg12d  34752  cdlemg12g  34755  cdlemg12  34756  cdlemg13a  34757  cdlemg13  34758  cdlemg17b  34768  cdlemg17dN  34769  cdlemg17dALTN  34770  cdlemg17e  34771  cdlemg17f  34772  cdlemg17i  34775  cdlemg17pq  34778  cdlemg17bq  34779  cdlemg17iqN  34780  cdlemg18d  34787  cdlemg18  34788  cdlemg19a  34789  cdlemg19  34790  cdlemg21  34792  cdlemg27a  34798  cdlemg28a  34799  cdlemg31b0N  34800  cdlemg27b  34802  cdlemg31c  34805  cdlemg33b0  34807  cdlemg33c0  34808  cdlemg28  34810  cdlemg33a  34812  cdlemg33  34817  cdlemg36  34820  ltrnco  34825  cdlemg44  34839  cdlemg47  34842  tendococl  34878  tendoplcl  34887  cdlemh1  34921  cdlemh2  34922  cdlemh  34923  cdlemi  34926  tendocan  34930  cdlemk5  34942  cdlemk6  34943  cdlemk7  34954  cdlemk11  34955  cdlemk12  34956  cdlemkole  34959  cdlemk14  34960  cdlemk15  34961  cdlemk16a  34962  cdlemk16  34963  cdlemk18  34974  cdlemk19  34975  cdlemk7u  34976  cdlemk11u  34977  cdlemk12u  34978  cdlemk21N  34979  cdlemk20  34980  cdlemkoatnle-2N  34981  cdlemk13-2N  34982  cdlemkole-2N  34983  cdlemk14-2N  34984  cdlemk15-2N  34985  cdlemk16-2N  34986  cdlemk17-2N  34987  cdlemk18-2N  34992  cdlemk19-2N  34993  cdlemk7u-2N  34994  cdlemk11u-2N  34995  cdlemk12u-2N  34996  cdlemk21-2N  34997  cdlemk20-2N  34998  cdlemk22  34999  cdlemk27-3  35013  cdlemk33N  35015  cdlemk11ta  35035  cdlemkid3N  35039  cdlemk11tc  35051  cdlemk11t  35052  cdlemk45  35053  cdlemk46  35054  cdlemk47  35055  cdlemk48  35056  cdlemk49  35057  cdlemk50  35058  cdlemk51  35059  cdlemk52  35060  cdlemk53a  35061  cdlemk55b  35066  cdlemkyyN  35068  cdlemk55u1  35071  cdlemk39u1  35073  cdlemk56  35077  cdlemm10N  35225  dihord1  35325  dihord2a  35326  dihord2b  35327  dihord10  35330  dihord4  35365  dihord5apre  35369  dihglblem2N  35401  dihjatc1  35418  dihjatc2N  35419  dihjatc3  35420  dihmeetlem15N  35428  dihmeetlem20N  35433  mapdpglem24  35811  hdmap14lem11  35988  hdmap14lem12  35989  mzpsubst  36129  monotuz  36324  congmul  36352  congsub  36355  ntrclsiso  37185  ntrclskb  37187  ntrclsk3  37188  infleinf  38330  mullimc  38484  mullimcf  38491  0ellimcdiv  38517  limclner  38519  sge0xaddlem2  39128  lincdifsn  42006
  Copyright terms: Public domain W3C validator