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

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

Proof of Theorem simp23r
StepHypRef Expression
1 simp3r 1244 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant2 1128 1 ((𝜏 ∧ (𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  ax5seglem6  26034  lshpkrlem5  34922  lplnexllnN  35372  4atexlemutvt  35862  cdlemc5  36004  cdlemd2  36008  cdleme0moN  36034  cdleme3h  36044  cdleme5  36049  cdleme9  36062  cdleme11l  36078  cdleme14  36082  cdleme15c  36085  cdleme16b  36088  cdleme16d  36090  cdleme16e  36091  cdlemednpq  36108  cdleme20bN  36119  cdleme20j  36127  cdleme20l2  36130  cdleme20l  36131  cdleme22cN  36151  cdleme22d  36152  cdleme22e  36153  cdleme22f  36155  cdleme26fALTN  36171  cdleme26f  36172  cdleme26f2ALTN  36173  cdleme26f2  36174  cdleme27a  36176  cdleme32b  36251  cdleme32d  36253  cdleme32f  36255  cdleme39n  36275  cdleme40n  36277  cdlemg2fv2  36409  cdlemg17h  36477  cdlemg27b  36505  cdlemg28b  36512  cdlemg28  36513  cdlemg29  36514  cdlemg33a  36515  cdlemg33d  36518  cdlemk7u-2N  36697  cdlemk11u-2N  36698  cdlemk12u-2N  36699  cdlemk26-3  36715  cdlemk27-3  36716  cdlemkfid3N  36734  cdlemn11c  37019
  Copyright terms: Public domain W3C validator