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

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

Proof of Theorem simp23r
StepHypRef Expression
1 simp3r 1088 . 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  25731  lshpkrlem5  33916  lplnexllnN  34365  4atexlemutvt  34855  cdlemc5  34997  cdlemd2  35001  cdleme0moN  35027  cdleme3h  35037  cdleme5  35042  cdleme9  35055  cdleme11l  35071  cdleme14  35075  cdleme15c  35078  cdleme16b  35081  cdleme16d  35083  cdleme16e  35084  cdlemednpq  35101  cdleme20bN  35113  cdleme20j  35121  cdleme20l2  35124  cdleme20l  35125  cdleme22cN  35145  cdleme22d  35146  cdleme22e  35147  cdleme22f  35149  cdleme26fALTN  35165  cdleme26f  35166  cdleme26f2ALTN  35167  cdleme26f2  35168  cdleme27a  35170  cdleme32b  35245  cdleme32d  35247  cdleme32f  35249  cdleme39n  35269  cdleme40n  35271  cdlemg2fv2  35403  cdlemg17h  35471  cdlemg27b  35499  cdlemg28b  35506  cdlemg28  35507  cdlemg29  35508  cdlemg33a  35509  cdlemg33d  35512  cdlemk7u-2N  35691  cdlemk11u-2N  35692  cdlemk12u-2N  35693  cdlemk26-3  35709  cdlemk27-3  35710  cdlemkfid3N  35728  cdlemn11c  36013
  Copyright terms: Public domain W3C validator