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

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

Proof of Theorem simp23r
StepHypRef Expression
1 simp3r 1199 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant2 1131 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:  ax5seglem6  26731  lshpkrlem5  36403  lplnexllnN  36853  4atexlemutvt  37343  cdlemc5  37484  cdlemd2  37488  cdleme0moN  37514  cdleme3h  37524  cdleme5  37529  cdleme9  37542  cdleme11l  37558  cdleme14  37562  cdleme15c  37565  cdleme16b  37568  cdleme16d  37570  cdleme16e  37571  cdlemednpq  37588  cdleme20bN  37599  cdleme20j  37607  cdleme20l2  37610  cdleme20l  37611  cdleme22cN  37631  cdleme22d  37632  cdleme22e  37633  cdleme22f  37635  cdleme26fALTN  37651  cdleme26f  37652  cdleme26f2ALTN  37653  cdleme26f2  37654  cdleme27a  37656  cdleme32b  37731  cdleme32d  37733  cdleme32f  37735  cdleme39n  37755  cdleme40n  37757  cdlemg2fv2  37889  cdlemg17h  37957  cdlemg27b  37985  cdlemg28b  37992  cdlemg28  37993  cdlemg29  37994  cdlemg33a  37995  cdlemg33d  37998  cdlemk7u-2N  38177  cdlemk11u-2N  38178  cdlemk12u-2N  38179  cdlemk26-3  38195  cdlemk27-3  38196  cdlemkfid3N  38214  cdlemn11c  38498
  Copyright terms: Public domain W3C validator