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

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

Proof of Theorem simp31r
StepHypRef Expression
1 simp1r 1241 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
213ad2ant3 1130 1 ((𝜏𝜂 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072 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 385  df-3an 1074 This theorem is referenced by:  ps-2c  35317  cdlema1N  35580  cdlemednpq  36089  cdleme19e  36097  cdleme20h  36106  cdleme20j  36108  cdleme20l2  36111  cdleme20m  36113  cdleme22a  36130  cdleme22cN  36132  cdleme22f2  36137  cdleme26f2ALTN  36154  cdleme37m  36252  cdlemg12f  36438  cdlemg12g  36439  cdlemg12  36440  cdlemg28a  36483  cdlemg29  36495  cdlemg33a  36496  cdlemg36  36504  cdlemk16a  36646  cdlemk21-2N  36681  cdlemk54  36748  dihord10  37014
 Copyright terms: Public domain W3C validator