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

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

Proof of Theorem simp23l
StepHypRef Expression
1 simp3l 1087 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant2 1081 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:  ax5seglem6  25727  lshpkrlem5  33908  lplnexllnN  34357  4atexlemt  34846  4atex2  34870  4atex3  34874  trlval4  34982  cdlemc5  34989  cdlemc6  34990  cdlemd2  34993  cdleme0e  35011  cdleme0moN  35019  cdleme3g  35028  cdleme3h  35029  cdleme3  35031  cdleme4  35032  cdleme5  35034  cdleme9  35047  cdleme11fN  35058  cdleme11j  35061  cdleme11k  35062  cdleme11l  35063  cdleme11  35064  cdleme14  35067  cdleme15a  35068  cdleme15b  35069  cdleme15c  35070  cdleme16b  35073  cdleme16c  35074  cdleme16d  35075  cdleme16e  35076  cdleme16f  35077  cdleme17d1  35083  cdleme18c  35087  cdlemednpq  35093  cdleme19c  35100  cdleme20bN  35105  cdleme20d  35107  cdleme20f  35109  cdleme20g  35110  cdleme20h  35111  cdleme20j  35113  cdleme20l2  35116  cdleme20l  35117  cdleme20m  35118  cdleme22cN  35137  cdleme22d  35138  cdleme22e  35139  cdleme22f  35141  cdleme26fALTN  35157  cdleme26f  35158  cdleme26f2ALTN  35159  cdleme26f2  35160  cdleme27a  35162  cdleme28a  35165  cdlemefs44  35221  cdlemefs45ee  35225  cdleme32b  35237  cdleme32c  35238  cdleme32e  35240  cdleme35sn2aw  35253  cdleme37m  35257  cdleme39n  35261  cdleme40n  35263  cdleme40w  35265  cdleme42k  35279  cdlemeg47rv2  35305  cdlemeg46rjgN  35317  cdlemeg46rgv  35323  cdlemeg46req  35324  cdlemg2fv2  35395  cdlemg17h  35463  cdlemg31b0a  35490  cdlemg27b  35491  cdlemg31d  35495  cdlemg28b  35498  cdlemg28  35499  cdlemg29  35500  cdlemg33a  35501  cdlemg33b  35502  cdlemg33c  35503  cdlemg33d  35504  cdlemg33e  35505  cdlemg44a  35526  cdlemk7u-2N  35683  cdlemk11u-2N  35684  cdlemk12u-2N  35685  cdlemk26-3  35701  cdlemk27-3  35702  cdlemkfid3N  35720  cdlemn2  35991  cdlemn10  36002  cdlemn11c  36005
  Copyright terms: Public domain W3C validator