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

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

Proof of Theorem simp11r
StepHypRef Expression
1 simp1r 1084 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
213ad2ant1 1080 1 ((((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜏𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  pceu  15486  maduf  20379  nllyrest  21212  exatleN  34205  2llnjaN  34367  2lplnja  34420  dalemceb  34439  pclfinN  34701  lhpexle3lem  34812  lhpmcvr5N  34828  lhpmcvr6N  34829  lhp2at0  34833  4atexlemw  34849  cdlemd2  35001  cdlemd4  35003  cdleme7aa  35044  cdleme7c  35047  cdleme7d  35048  cdleme7e  35049  cdleme7ga  35050  cdleme7  35051  cdleme15a  35076  cdleme15b  35077  cdleme15d  35079  cdleme15  35080  cdleme16b  35081  cdleme16c  35082  cdleme16d  35083  cdleme16e  35084  cdleme16f  35085  cdleme18d  35097  cdleme19b  35107  cdleme19d  35109  cdleme19e  35110  cdleme20d  35115  cdleme20e  35116  cdleme20f  35117  cdleme20g  35118  cdleme20h  35119  cdleme20j  35121  cdleme20k  35122  cdleme20l1  35123  cdleme20l2  35124  cdleme20l  35125  cdleme20m  35126  cdleme21c  35130  cdleme21ct  35132  cdleme22cN  35145  cdleme22f  35149  cdleme22g  35151  cdleme23a  35152  cdleme23b  35153  cdleme23c  35154  cdleme25a  35156  cdleme25c  35158  cdleme25dN  35159  cdleme26ee  35163  cdleme26eALTN  35164  cdleme27N  35172  cdleme28a  35173  cdleme28b  35174  cdleme29ex  35177  cdlemefr29exN  35205  cdleme32b  35245  cdleme32c  35246  cdleme32e  35248  cdleme35b  35253  cdleme35c  35254  cdleme35d  35255  cdleme35e  35256  cdleme35f  35257  cdleme42h  35285  cdleme42i  35286  cdleme42k  35287  cdleme48bw  35305  cdlemeg46frv  35328  cdlemeg46vrg  35330  cdlemeg46rgv  35331  cdlemeg46req  35332  cdlemf1  35364  trlord  35372  cdlemg7fvbwN  35410  cdlemg10  35444  cdlemg12e  35450  cdlemg12f  35451  cdlemg19a  35486  cdlemg31c  35502  cdlemg33c0  35505  cdlemg35  35516  tendococl  35575  cdlemh2  35619  cdlemh  35620  cdlemi  35623  cdlemk5  35639  cdlemk7  35651  cdlemk11  35652  cdlemk5u  35664  cdlemkj  35666  cdlemkuv2  35670  cdlemk7u  35673  cdlemk11u  35674  cdlemk26-3  35709  cdlemk11t  35749  cdlemk52  35757  cdlemk53a  35758  dihord1  36022  dihord2a  36023  dihord2b  36024  dihord11b  36026  dihord11c  36028  dihord2pre  36029  dihord2pre2  36030  dihord5apre  36066  dihmeetlem1N  36094  dihglblem2N  36098  dihglblem3N  36099  dihglbcpreN  36104  dihmeetlem3N  36109  dihjatc1  36115  suplesup  39050  limsupre  39305  sge0xaddlem2  39984
  Copyright terms: Public domain W3C validator