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

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

Proof of Theorem simp31l
StepHypRef Expression
1 simp1l 1239 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
213ad2ant3 1129 1 ((𝜏𝜂 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  ps-2c  35336  cdlema1N  35599  trlval3  35996  cdleme12  36080  cdlemednpq  36108  cdleme19d  36115  cdleme19e  36116  cdleme20f  36123  cdleme20h  36125  cdleme20l2  36130  cdleme20l  36131  cdleme20m  36132  cdleme21j  36145  cdleme22a  36149  cdleme22cN  36151  cdleme22f2  36156  cdleme32b  36251  cdlemg12f  36457  cdlemg12g  36458  cdlemg12  36459  cdlemg28a  36502  cdlemg31b0N  36503  cdlemg29  36514  cdlemg33a  36515  cdlemg36  36523  cdlemg42  36538  cdlemk16a  36665  cdlemk21-2N  36700  cdlemk32  36706  cdlemkid2  36733  cdlemk54  36767  cdlemk55a  36768  dihord10  37033
  Copyright terms: Public domain W3C validator