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

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

Proof of Theorem simp31r
StepHypRef Expression
1 simp1r 1084 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
213ad2ant3 1082 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:  ps-2c  34291  cdlema1N  34554  cdlemednpq  35063  cdleme19e  35072  cdleme20h  35081  cdleme20j  35083  cdleme20l2  35086  cdleme20m  35088  cdleme22a  35105  cdleme22cN  35107  cdleme22f2  35112  cdleme26f2ALTN  35129  cdleme37m  35227  cdlemg12f  35413  cdlemg12g  35414  cdlemg12  35415  cdlemg28a  35458  cdlemg29  35470  cdlemg33a  35471  cdlemg36  35479  cdlemk16a  35621  cdlemk21-2N  35656  cdlemk54  35723  dihord10  35989
  Copyright terms: Public domain W3C validator