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 399  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 210  df-an 400  df-3an 1086
This theorem is referenced by:  ps-2c  36796  cdlema1N  37059  cdlemednpq  37567  cdleme19e  37575  cdleme20h  37584  cdleme20j  37586  cdleme20l2  37589  cdleme20m  37591  cdleme22a  37608  cdleme22cN  37610  cdleme22f2  37615  cdleme26f2ALTN  37632  cdleme37m  37730  cdlemg12f  37916  cdlemg12g  37917  cdlemg12  37918  cdlemg28a  37961  cdlemg29  37973  cdlemg33a  37974  cdlemg36  37982  cdlemk16a  38124  cdlemk21-2N  38159  cdlemk54  38226  dihord10  38491
  Copyright terms: Public domain W3C validator