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

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

Proof of Theorem simp12
StepHypRef Expression
1 simp2 1134 . 2 ((𝜑𝜓𝜒) → 𝜓)
213ad2ant1 1130 1 (((𝜑𝜓𝜒) ∧ 𝜃𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  simp112  1300  simp212  1309  simp312  1318  dvdsgcd  15892  coprimeprodsq  16145  pythagtriplem4  16156  pythagtriplem13  16164  pythagtriplem14  16165  pythagtriplem16  16167  pythagtrip  16171  pceu  16183  mremre  16877  lsmpropd  18805  m2cpminvid  21367  decpmatid  21384  mply1topmatcllem  21417  cmpsublem  22013  isfil2  22470  cxple2a  25299  isosctr  25416  brbtwn2  26708  colinearalg  26713  ax5seg  26741  axcontlem4  26770  bayesth  31782  bnj1204  32369  bnj1279  32375  nolesgn2o  33263  nolesgn2ores  33264  nolt02o  33284  ofscom  33553  btwndiff  33573  ifscgr  33590  brofs2  33623  brifs2  33624  fscgr  33626  btwnconn1lem1  33633  btwnconn1lem2  33634  btwnconn1lem3  33635  btwnconn1lem4  33636  btwnconn1lem12  33644  seglecgr12im  33656  seglecgr12  33657  ivthALT  33768  islshpcv  36321  lkrshp  36373  lshpsmreu  36377  lshpkrlem5  36382  cvrval3  36681  4noncolr3  36721  4noncolr2  36722  4noncolr1  36723  athgt  36724  3dimlem2  36727  3dimlem3a  36728  3dimlem4a  36731  3dimlem4  36732  3dimlem4OLDN  36733  1cvratex  36741  hlatexch4  36749  ps-2b  36750  3atlem4  36754  llnnleat  36781  2atm  36795  ps-2c  36796  llnmlplnN  36807  lplnnlelln  36811  2atmat  36829  lvoli2  36849  lvolnlelln  36852  4atlem3b  36866  4atlem10  36874  4atlem11a  36875  4atlem11b  36876  4atlem12a  36878  lplncvrlvol2  36883  2lplnja  36887  dalemswapyz  36924  lneq2at  37046  2lnat  37052  cdlema1N  37059  cdlemb  37062  paddasslem15  37102  pmodlem1  37114  llnmod2i2  37131  llnexchb2lem  37136  dalawlem1  37139  dalawlem3  37141  dalawlem4  37142  dalawlem6  37144  dalawlem7  37145  dalawlem9  37147  dalawlem10  37148  dalawlem11  37149  dalawlem12  37150  dalawlem13  37151  dalawlem15  37153  osumcllem5N  37228  osumcllem6N  37229  osumcllem7N  37230  osumcllem9N  37232  osumcllem10N  37233  osumcllem11N  37234  pl42lem1N  37247  lhpmcvr5N  37295  lhp2atne  37302  lhp2at0ne  37304  4atexlempw  37317  4atexlemex6  37342  4atexlem7  37343  ldilco  37384  ltrneq  37417  trlval2  37431  trlnidat  37441  cdlemd7  37472  cdleme7aa  37510  cdleme7c  37513  cdleme7d  37514  cdleme7e  37515  cdleme7ga  37516  cdleme7  37517  cdleme11c  37529  cdleme11e  37531  cdleme11l  37537  cdleme11  37538  cdleme14  37541  cdleme15a  37542  cdleme15c  37544  cdleme16b  37547  cdleme16c  37548  cdleme16d  37549  cdleme16e  37550  cdleme16f  37551  cdleme0nex  37558  cdleme18d  37563  cdleme19b  37572  cdleme19d  37574  cdleme19e  37575  cdleme20f  37582  cdleme20k  37587  cdleme20l1  37588  cdleme20l2  37589  cdleme20l  37590  cdleme20m  37591  cdleme21a  37593  cdleme21b  37594  cdleme21ct  37597  cdleme21d  37598  cdleme21e  37599  cdleme21f  37600  cdleme21h  37602  cdleme21i  37603  cdleme22eALTN  37613  cdleme22f2  37615  cdleme22g  37616  cdleme24  37620  cdleme25a  37621  cdleme25c  37623  cdleme25dN  37624  cdleme26e  37627  cdleme26ee  37628  cdleme26eALTN  37629  cdleme27N  37637  cdleme28a  37638  cdleme28b  37639  cdleme28  37641  cdlemefr32sn2aw  37672  cdlemefs32sn1aw  37682  cdleme43fsv1snlem  37688  cdleme41sn3a  37701  cdleme32c  37711  cdleme32e  37713  cdleme32le  37715  cdleme35a  37716  cdleme35b  37718  cdleme35c  37719  cdleme35e  37721  cdleme35f  37722  cdleme36a  37728  cdleme36m  37729  cdleme39a  37733  cdleme40m  37735  cdleme40n  37736  cdleme43bN  37758  cdleme43dN  37760  cdleme46f2g2  37761  cdleme46f2g1  37762  cdleme17d2  37763  cdleme4gfv  37775  cdlemeg49le  37779  cdlemeg46c  37781  cdlemeg46fvaw  37784  cdlemeg46nlpq  37785  cdlemeg46gfre  37800  cdleme50trn2  37819  cdleme  37828  cdlemg2idN  37864  cdlemg7fvbwN  37875  cdlemg10bALTN  37904  cdlemg10a  37908  cdlemg12d  37914  cdlemg12g  37917  cdlemg12  37918  cdlemg13a  37919  cdlemg13  37920  cdlemg17b  37930  cdlemg17dN  37931  cdlemg17dALTN  37932  cdlemg17e  37933  cdlemg17f  37934  cdlemg17i  37937  cdlemg17pq  37940  cdlemg17bq  37941  cdlemg17iqN  37942  cdlemg18d  37949  cdlemg18  37950  cdlemg19a  37951  cdlemg19  37952  cdlemg21  37954  cdlemg27a  37960  cdlemg28a  37961  cdlemg31b0N  37962  cdlemg27b  37964  cdlemg31c  37967  cdlemg33b0  37969  cdlemg33c0  37970  cdlemg28  37972  cdlemg33a  37974  cdlemg33  37979  cdlemg36  37982  ltrnco  37987  cdlemg44  38001  cdlemg47  38004  tendococl  38040  tendoplcl  38049  cdlemh1  38083  cdlemh2  38084  cdlemh  38085  cdlemi  38088  tendocan  38092  cdlemk5  38104  cdlemk6  38105  cdlemk7  38116  cdlemk11  38117  cdlemk12  38118  cdlemkole  38121  cdlemk14  38122  cdlemk15  38123  cdlemk16a  38124  cdlemk16  38125  cdlemk18  38136  cdlemk19  38137  cdlemk7u  38138  cdlemk11u  38139  cdlemk12u  38140  cdlemk21N  38141  cdlemk20  38142  cdlemkoatnle-2N  38143  cdlemk13-2N  38144  cdlemkole-2N  38145  cdlemk14-2N  38146  cdlemk15-2N  38147  cdlemk16-2N  38148  cdlemk17-2N  38149  cdlemk18-2N  38154  cdlemk19-2N  38155  cdlemk7u-2N  38156  cdlemk11u-2N  38157  cdlemk12u-2N  38158  cdlemk21-2N  38159  cdlemk20-2N  38160  cdlemk22  38161  cdlemk27-3  38175  cdlemk33N  38177  cdlemk11ta  38197  cdlemkid3N  38201  cdlemk11tc  38213  cdlemk11t  38214  cdlemk45  38215  cdlemk46  38216  cdlemk47  38217  cdlemk48  38218  cdlemk49  38219  cdlemk50  38220  cdlemk51  38221  cdlemk52  38222  cdlemk53a  38223  cdlemk55b  38228  cdlemkyyN  38230  cdlemk55u1  38233  cdlemk39u1  38235  cdlemk56  38239  cdlemm10N  38386  dihord1  38486  dihord2a  38487  dihord2b  38488  dihord10  38491  dihord4  38526  dihord5apre  38530  dihglblem2N  38562  dihjatc1  38579  dihjatc2N  38580  dihjatc3  38581  dihmeetlem15N  38589  dihmeetlem20N  38594  mapdpglem24  38972  hdmap14lem11  39146  hdmap14lem12  39147  mzpsubst  39633  monotuz  39826  congmul  39852  congsub  39855  ntrclsiso  40717  ntrclskb  40719  ntrclsk3  40720  infleinf  41957  mullimc  42211  mullimcf  42218  0ellimcdiv  42244  limclner  42246  sge0xaddlem2  43026  lincdifsn  44786  itschlc0yqe  45127  itscnhlc0xyqsol  45132  itsclc0xyqsolr  45136  itsclquadeu  45144
  Copyright terms: Public domain W3C validator