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

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

Proof of Theorem simp31l
StepHypRef Expression
1 simp1l 1198 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
213ad2ant3 1136 1 ((𝜏𝜂 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  ps-2c  38305  cdlema1N  38568  trlval3  38964  cdleme12  39048  cdlemednpq  39076  cdleme19d  39083  cdleme19e  39084  cdleme20f  39091  cdleme20h  39093  cdleme20l2  39098  cdleme20l  39099  cdleme20m  39100  cdleme21j  39113  cdleme22a  39117  cdleme22cN  39119  cdleme22f2  39124  cdleme32b  39219  cdlemg12f  39425  cdlemg12g  39426  cdlemg12  39427  cdlemg28a  39470  cdlemg31b0N  39471  cdlemg29  39482  cdlemg33a  39483  cdlemg36  39491  cdlemg42  39506  cdlemk16a  39633  cdlemk21-2N  39668  cdlemk32  39674  cdlemkid2  39701  cdlemk54  39735  cdlemk55a  39736  dihord10  40000
  Copyright terms: Public domain W3C validator