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

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

Proof of Theorem simp11r
StepHypRef Expression
1 simp1r 1195 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
213ad2ant1 1130 1 ((((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜏𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  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:  pceu  16177  maduf  21250  nllyrest  22095  exatleN  36699  2llnjaN  36861  2lplnja  36914  dalemceb  36933  pclfinN  37195  lhpexle3lem  37306  lhpmcvr5N  37322  lhpmcvr6N  37323  lhp2at0  37327  4atexlemw  37343  cdlemd2  37494  cdlemd4  37496  cdleme7aa  37537  cdleme7c  37540  cdleme7d  37541  cdleme7e  37542  cdleme7ga  37543  cdleme7  37544  cdleme15a  37569  cdleme15b  37570  cdleme15d  37572  cdleme15  37573  cdleme16b  37574  cdleme16c  37575  cdleme16d  37576  cdleme16e  37577  cdleme16f  37578  cdleme18d  37590  cdleme19b  37599  cdleme19d  37601  cdleme19e  37602  cdleme20d  37607  cdleme20e  37608  cdleme20f  37609  cdleme20g  37610  cdleme20h  37611  cdleme20j  37613  cdleme20k  37614  cdleme20l1  37615  cdleme20l2  37616  cdleme20l  37617  cdleme20m  37618  cdleme21c  37622  cdleme21ct  37624  cdleme22cN  37637  cdleme22f  37641  cdleme22g  37643  cdleme23a  37644  cdleme23b  37645  cdleme23c  37646  cdleme25a  37648  cdleme25c  37650  cdleme25dN  37651  cdleme26ee  37655  cdleme26eALTN  37656  cdleme27N  37664  cdleme28a  37665  cdleme28b  37666  cdleme29ex  37669  cdlemefr29exN  37697  cdleme32b  37737  cdleme32c  37738  cdleme32e  37740  cdleme35b  37745  cdleme35c  37746  cdleme35d  37747  cdleme35e  37748  cdleme35f  37749  cdleme42h  37777  cdleme42i  37778  cdleme42k  37779  cdleme48bw  37797  cdlemeg46frv  37820  cdlemeg46vrg  37822  cdlemeg46rgv  37823  cdlemeg46req  37824  cdlemf1  37856  trlord  37864  cdlemg7fvbwN  37902  cdlemg10  37936  cdlemg12e  37942  cdlemg12f  37943  cdlemg19a  37978  cdlemg31c  37994  cdlemg33c0  37997  cdlemg35  38008  tendococl  38067  cdlemh2  38111  cdlemh  38112  cdlemi  38115  cdlemk5  38131  cdlemk7  38143  cdlemk11  38144  cdlemk5u  38156  cdlemkj  38158  cdlemkuv2  38162  cdlemk7u  38165  cdlemk11u  38166  cdlemk26-3  38201  cdlemk11t  38241  cdlemk52  38249  cdlemk53a  38250  dihord1  38513  dihord2a  38514  dihord2b  38515  dihord11b  38517  dihord11c  38519  dihord2pre  38520  dihord2pre2  38521  dihord5apre  38557  dihmeetlem1N  38585  dihglblem2N  38589  dihglblem3N  38590  dihglbcpreN  38595  dihmeetlem3N  38600  dihjatc1  38606  suplesup  41964  limsupre  42276  sge0xaddlem2  43066  itscnhlc0yqe  45166  itscnhlc0xyqsol  45172  itsclquadb  45183  itsclquadeu  45184
  Copyright terms: Public domain W3C validator