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

Theorem simp11r 1285
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp11r ((((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜏𝜂) → 𝜓)

Proof of Theorem simp11r
StepHypRef Expression
1 simp1r 1198 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
213ad2ant1 1133 1 ((((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜏𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087
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 206  df-an 397  df-3an 1089
This theorem is referenced by:  pceu  16717  maduf  21988  nllyrest  22835  exatleN  37858  2llnjaN  38020  2lplnja  38073  dalemceb  38092  pclfinN  38354  lhpexle3lem  38465  lhpmcvr5N  38481  lhpmcvr6N  38482  lhp2at0  38486  4atexlemw  38502  cdlemd2  38653  cdlemd4  38655  cdleme7aa  38696  cdleme7c  38699  cdleme7d  38700  cdleme7e  38701  cdleme7ga  38702  cdleme7  38703  cdleme15a  38728  cdleme15b  38729  cdleme15d  38731  cdleme15  38732  cdleme16b  38733  cdleme16c  38734  cdleme16d  38735  cdleme16e  38736  cdleme16f  38737  cdleme18d  38749  cdleme19b  38758  cdleme19d  38760  cdleme19e  38761  cdleme20d  38766  cdleme20e  38767  cdleme20f  38768  cdleme20g  38769  cdleme20h  38770  cdleme20j  38772  cdleme20k  38773  cdleme20l1  38774  cdleme20l2  38775  cdleme20l  38776  cdleme20m  38777  cdleme21c  38781  cdleme21ct  38783  cdleme22cN  38796  cdleme22f  38800  cdleme22g  38802  cdleme23a  38803  cdleme23b  38804  cdleme23c  38805  cdleme25a  38807  cdleme25c  38809  cdleme25dN  38810  cdleme26ee  38814  cdleme26eALTN  38815  cdleme27N  38823  cdleme28a  38824  cdleme28b  38825  cdleme29ex  38828  cdlemefr29exN  38856  cdleme32b  38896  cdleme32c  38897  cdleme32e  38899  cdleme35b  38904  cdleme35c  38905  cdleme35d  38906  cdleme35e  38907  cdleme35f  38908  cdleme42h  38936  cdleme42i  38937  cdleme42k  38938  cdleme48bw  38956  cdlemeg46frv  38979  cdlemeg46vrg  38981  cdlemeg46rgv  38982  cdlemeg46req  38983  cdlemf1  39015  trlord  39023  cdlemg7fvbwN  39061  cdlemg10  39095  cdlemg12e  39101  cdlemg12f  39102  cdlemg19a  39137  cdlemg31c  39153  cdlemg33c0  39156  cdlemg35  39167  tendococl  39226  cdlemh2  39270  cdlemh  39271  cdlemi  39274  cdlemk5  39290  cdlemk7  39302  cdlemk11  39303  cdlemk5u  39315  cdlemkj  39317  cdlemkuv2  39321  cdlemk7u  39324  cdlemk11u  39325  cdlemk26-3  39360  cdlemk11t  39400  cdlemk52  39408  cdlemk53a  39409  dihord1  39672  dihord2a  39673  dihord2b  39674  dihord11b  39676  dihord11c  39678  dihord2pre  39679  dihord2pre2  39680  dihord5apre  39716  dihmeetlem1N  39744  dihglblem2N  39748  dihglblem3N  39749  dihglbcpreN  39754  dihmeetlem3N  39759  dihjatc1  39765  suplesup  43549  limsupre  43854  sge0xaddlem2  44647  itscnhlc0yqe  46817  itscnhlc0xyqsol  46823  itsclquadb  46834  itsclquadeu  46835
  Copyright terms: Public domain W3C validator