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

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

Proof of Theorem simp31l
StepHypRef Expression
1 simp1l 1199 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
213ad2ant3 1137 1 ((𝜏𝜂 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089
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 1091
This theorem is referenced by:  ps-2c  37279  cdlema1N  37542  trlval3  37938  cdleme12  38022  cdlemednpq  38050  cdleme19d  38057  cdleme19e  38058  cdleme20f  38065  cdleme20h  38067  cdleme20l2  38072  cdleme20l  38073  cdleme20m  38074  cdleme21j  38087  cdleme22a  38091  cdleme22cN  38093  cdleme22f2  38098  cdleme32b  38193  cdlemg12f  38399  cdlemg12g  38400  cdlemg12  38401  cdlemg28a  38444  cdlemg31b0N  38445  cdlemg29  38456  cdlemg33a  38457  cdlemg36  38465  cdlemg42  38480  cdlemk16a  38607  cdlemk21-2N  38642  cdlemk32  38648  cdlemkid2  38675  cdlemk54  38709  cdlemk55a  38710  dihord10  38974
  Copyright terms: Public domain W3C validator