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

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

Proof of Theorem simp11
StepHypRef Expression
1 simp1 1128 . 2 ((𝜑𝜓𝜒) → 𝜑)
213ad2ant1 1125 1 (((𝜑𝜓𝜒) ∧ 𝜃𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  simp111  1294  simp211  1303  simp311  1312  omeulem1  8197  omeu  8200  ackbij1lem16  9645  coprimeprodsq  16133  pythagtriplem14  16153  pythagtrip  16159  mrelatglb  17782  subglsm  18728  lsmpropd  18732  mdetmul  21160  decpmatid  21306  isfil2  22392  filuni  22421  cxple2a  25209  isosctr  25326  brbtwn2  26618  colinearalg  26623  ax5seglem3  26644  clwwlknonex2  27815  measres  31380  bayesth  31596  nolesgn2o  33075  nolesgn2ores  33076  nolt02o  33096  ofscom  33365  btwndiff  33385  ifscgr  33402  brofs2  33435  brifs2  33436  fscgr  33438  btwnconn1lem1  33445  btwnconn1lem2  33446  btwnconn1lem3  33447  btwnconn1lem4  33448  btwnconn1lem5  33449  btwnconn1lem6  33450  btwnconn1lem7  33451  btwnconn1lem8  33452  btwnconn1lem9  33453  btwnconn1lem10  33454  btwnconn1lem11  33455  btwnconn1lem12  33456  seglecgr12im  33468  seglecgr12  33469  ivthALT  33580  eqlkr  36115  lkrshp  36121  lshpkrlem5  36130  cvrval3  36429  4noncolr3  36469  4noncolr2  36470  4noncolr1  36471  athgt  36472  3dimlem2  36475  3dimlem3a  36476  3dimlem4a  36479  3dimlem4  36480  3dimlem4OLDN  36481  3dim2  36484  1cvratex  36489  hlatexch4  36497  ps-2b  36498  3atlem1  36499  3atlem2  36500  3atlem4  36502  3atlem5  36503  3atlem6  36504  llnnleat  36529  2atm  36543  ps-2c  36544  llnmlplnN  36555  lplnnlelln  36559  2atmat  36577  2llnjN  36583  lvoli2  36597  lvolnlelln  36600  4atlem3b  36614  4atlem9  36619  4atlem10a  36620  4atlem10  36622  4atlem11a  36623  4atlem11b  36624  4atlem12a  36626  4atlem12b  36627  4at  36629  4at2  36630  lplncvrlvol2  36631  2lplnj  36636  dalemswapyz  36672  dath2  36753  lneq2at  36794  2lnat  36800  cdlema1N  36807  cdlemb  36810  paddasslem15  36850  pmodlem1  36862  llnmod2i2  36879  llnexchb2lem  36884  llnexchb2  36885  dalawlem1  36887  dalawlem3  36889  dalawlem4  36890  dalawlem5  36891  dalawlem6  36892  dalawlem7  36893  dalawlem8  36894  dalawlem9  36895  dalawlem10  36896  dalawlem11  36897  dalawlem12  36898  dalawlem13  36899  dalawlem15  36901  dalaw  36902  osumcllem5N  36976  osumcllem6N  36977  osumcllem7N  36978  osumcllem9N  36980  osumcllem10N  36981  osumcllem11N  36982  pl42lem1N  36995  lhpexle3lem  37027  lhpmcvr5N  37043  lhp2atne  37050  lhp2at0ne  37052  4atexlemswapqr  37079  4atexlemex6  37090  ldilco  37132  ltrneq  37165  trlval2  37179  trlnidat  37189  cdlemd2  37215  cdlemd7  37220  cdlemd8  37221  cdleme7aa  37258  cdleme7c  37261  cdleme7d  37262  cdleme7e  37263  cdleme7ga  37264  cdleme7  37265  cdleme11c  37277  cdleme11e  37279  cdleme11l  37285  cdleme11  37286  cdleme14  37289  cdleme15a  37290  cdleme15c  37292  cdleme16b  37295  cdleme16c  37296  cdleme16d  37297  cdleme16e  37298  cdleme16f  37299  cdleme0nex  37306  cdleme18d  37311  cdleme19b  37320  cdleme19d  37322  cdleme19e  37323  cdleme20f  37330  cdleme20i  37333  cdleme20k  37335  cdleme20l1  37336  cdleme20l2  37337  cdleme20l  37338  cdleme20m  37339  cdleme21a  37341  cdleme21b  37342  cdleme21ct  37345  cdleme21d  37346  cdleme21e  37347  cdleme21f  37348  cdleme21h  37350  cdleme22eALTN  37361  cdleme22f2  37363  cdleme22g  37364  cdleme26e  37375  cdleme26eALTN  37377  cdleme26fALTN  37378  cdleme26f  37379  cdleme26f2ALTN  37380  cdleme26f2  37381  cdleme28a  37386  cdleme28b  37387  cdleme28  37389  cdleme29ex  37390  cdleme29c  37392  cdlemefrs29cpre1  37414  cdlemefr29exN  37418  cdlemefr32sn2aw  37420  cdlemefr29bpre0N  37422  cdlemefr29clN  37423  cdlemefr32fvaN  37425  cdlemefr32fva1  37426  cdlemefs32sn1aw  37430  cdleme43fsv1snlem  37436  cdleme41sn3a  37449  cdleme32fva  37453  cdleme32b  37458  cdleme32d  37460  cdleme32e  37461  cdleme32f  37462  cdleme32le  37463  cdleme35a  37464  cdleme35fnpq  37465  cdleme35b  37466  cdleme35c  37467  cdleme35d  37468  cdleme35e  37469  cdleme35f  37470  cdleme36a  37476  cdleme36m  37477  cdleme37m  37478  cdleme39a  37481  cdleme39n  37482  cdleme40m  37483  cdleme40n  37484  cdleme42e  37495  cdleme42f  37496  cdleme42g  37497  cdleme43bN  37506  cdleme43cN  37507  cdleme43dN  37508  cdleme46f2g2  37509  cdleme46f2g1  37510  cdleme17d2  37511  cdleme48b  37519  cdleme4gfv  37523  cdlemeg49le  37527  cdlemeg46c  37529  cdlemeg46fvaw  37532  cdlemeg46nlpq  37533  cdlemeg46frv  37541  cdlemeg46rgv  37544  cdlemeg46req  37545  cdlemeg46gfre  37548  cdleme50trn1  37565  cdleme50trn2a  37566  cdleme50trn2  37567  cdleme  37576  cdlemf  37579  trlord  37585  cdlemg2ce  37608  cdlemg7fvbwN  37623  cdlemg7aN  37641  cdlemg10bALTN  37652  cdlemg10a  37656  cdlemg10  37657  cdlemg12d  37662  cdlemg12f  37664  cdlemg12g  37665  cdlemg12  37666  cdlemg13a  37667  cdlemg13  37668  cdlemg17b  37678  cdlemg17dN  37679  cdlemg17dALTN  37680  cdlemg17e  37681  cdlemg17f  37682  cdlemg17g  37683  cdlemg17h  37684  cdlemg17i  37685  cdlemg17pq  37688  cdlemg17bq  37689  cdlemg17iqN  37690  cdlemg17  37693  cdlemg18d  37697  cdlemg18  37698  cdlemg19a  37699  cdlemg19  37700  cdlemg21  37702  cdlemg27a  37708  cdlemg28a  37709  cdlemg31b0N  37710  cdlemg27b  37712  cdlemg33b0  37717  cdlemg28b  37719  cdlemg28  37720  cdlemg33a  37722  cdlemg33  37727  cdlemg34  37728  cdlemg35  37729  cdlemg36  37730  ltrnco  37735  trlcone  37744  cdlemg44  37749  cdlemg47  37752  cdlemg48  37753  tendococl  37788  tendoplcl  37797  cdlemh1  37831  cdlemi  37836  cdlemj1  37837  cdlemj2  37838  tendocan  37840  cdlemk6  37853  cdlemki  37857  cdlemksat  37862  cdlemksv2  37863  cdlemk7  37864  cdlemk11  37865  cdlemk12  37866  cdlemkoatnle  37867  cdlemkole  37869  cdlemk14  37870  cdlemk15  37871  cdlemk16a  37872  cdlemk16  37873  cdlemk17  37874  cdlemk1u  37875  cdlemk5u  37877  cdlemk6u  37878  cdlemkuat  37882  cdlemk18  37884  cdlemk19  37885  cdlemk12u  37888  cdlemk21N  37889  cdlemk20  37890  cdlemkoatnle-2N  37891  cdlemk13-2N  37892  cdlemkole-2N  37893  cdlemk14-2N  37894  cdlemk15-2N  37895  cdlemk16-2N  37896  cdlemk17-2N  37897  cdlemk18-2N  37902  cdlemk19-2N  37903  cdlemk7u-2N  37904  cdlemk11u-2N  37905  cdlemk12u-2N  37906  cdlemk21-2N  37907  cdlemk20-2N  37908  cdlemk22  37909  cdlemk23-3  37918  cdlemk25-3  37920  cdlemk26b-3  37921  cdlemk27-3  37923  cdlemk28-3  37924  cdlemk33N  37925  cdlemk37  37930  cdlemky  37942  cdlemk11ta  37945  cdlemkid3N  37949  cdlemk11tc  37961  cdlemk11t  37962  cdlemk45  37963  cdlemk46  37964  cdlemk47  37965  cdlemk48  37966  cdlemk49  37967  cdlemk50  37968  cdlemk51  37969  cdlemk52  37970  cdlemk55b  37976  cdlemkyyN  37978  cdlemk55u1  37981  cdlemk55u  37982  cdlemk39u1  37983  cdlemk39u  37984  cdlemk56  37987  cdleml3N  37994  cdleml4N  37995  cdlemm10N  38134  dihord1  38234  dihord2a  38235  dihord2b  38236  dihord10  38239  dihord11c  38240  dihord2pre  38241  dihord4  38274  dihord5apre  38278  dihmeetlem1N  38306  dihglbcpreN  38316  dihjatc1  38327  dihjatc3  38329  dihmeetlem13N  38335  dihmeetlem20N  38342  baerlem3lem2  38726  baerlem5alem2  38727  baerlem5blem2  38728  hdmap14lem11  38894  hdmap14lem12  38895  monotuz  39416  congmul  39442  congsub  39445  rpnnen3lem  39506  ntrclsiso  40295  ntrclskb  40297  ntrclsk3  40298  wessf1ornlem  41321  infleinf  41516  lincdifsn  44407  itsclc0yqe  44676  itsclc0xyqsolr  44684
  Copyright terms: Public domain W3C validator