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

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

Proof of Theorem simp31r
StepHypRef Expression
1 simp1r 1195 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
213ad2ant3 1132 1 ((𝜏𝜂 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  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 206  df-an 395  df-3an 1086
This theorem is referenced by:  ps-2c  39131  cdlema1N  39394  cdlemednpq  39902  cdleme19e  39910  cdleme20h  39919  cdleme20j  39921  cdleme20l2  39924  cdleme20m  39926  cdleme22a  39943  cdleme22cN  39945  cdleme22f2  39950  cdleme26f2ALTN  39967  cdleme37m  40065  cdlemg12f  40251  cdlemg12g  40252  cdlemg12  40253  cdlemg28a  40296  cdlemg29  40308  cdlemg33a  40309  cdlemg36  40317  cdlemk16a  40459  cdlemk21-2N  40494  cdlemk54  40561  dihord10  40826
  Copyright terms: Public domain W3C validator