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

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

Proof of Theorem simp31r
StepHypRef Expression
1 simp1r 1239 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
213ad2ant3 1128 1 ((𝜏𝜂 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1070
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 1072
This theorem is referenced by:  ps-2c  35329  cdlema1N  35592  cdlemednpq  36101  cdleme19e  36109  cdleme20h  36118  cdleme20j  36120  cdleme20l2  36123  cdleme20m  36125  cdleme22a  36142  cdleme22cN  36144  cdleme22f2  36149  cdleme26f2ALTN  36166  cdleme37m  36264  cdlemg12f  36450  cdlemg12g  36451  cdlemg12  36452  cdlemg28a  36495  cdlemg29  36507  cdlemg33a  36508  cdlemg36  36516  cdlemk16a  36658  cdlemk21-2N  36693  cdlemk54  36760  dihord10  37026
  Copyright terms: Public domain W3C validator