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

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

Proof of Theorem simp31l
StepHypRef Expression
1 simp1l 1247 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
213ad2ant3 1158 1 ((𝜏𝜂 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  ps-2c  35306  cdlema1N  35569  trlval3  35966  cdleme12  36050  cdlemednpq  36078  cdleme19d  36085  cdleme19e  36086  cdleme20f  36093  cdleme20h  36095  cdleme20l2  36100  cdleme20l  36101  cdleme20m  36102  cdleme21j  36115  cdleme22a  36119  cdleme22cN  36121  cdleme22f2  36126  cdleme32b  36221  cdlemg12f  36427  cdlemg12g  36428  cdlemg12  36429  cdlemg28a  36472  cdlemg31b0N  36473  cdlemg29  36484  cdlemg33a  36485  cdlemg36  36493  cdlemg42  36508  cdlemk16a  36635  cdlemk21-2N  36670  cdlemk32  36676  cdlemkid2  36703  cdlemk54  36737  cdlemk55a  36738  dihord10  37002
  Copyright terms: Public domain W3C validator