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

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

Proof of Theorem simp31l
StepHypRef Expression
1 simp1l 1190 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
213ad2ant3 1128 1 ((𝜏𝜂 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1080
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 208  df-an 397  df-3an 1082
This theorem is referenced by:  ps-2c  36214  cdlema1N  36477  trlval3  36873  cdleme12  36957  cdlemednpq  36985  cdleme19d  36992  cdleme19e  36993  cdleme20f  37000  cdleme20h  37002  cdleme20l2  37007  cdleme20l  37008  cdleme20m  37009  cdleme21j  37022  cdleme22a  37026  cdleme22cN  37028  cdleme22f2  37033  cdleme32b  37128  cdlemg12f  37334  cdlemg12g  37335  cdlemg12  37336  cdlemg28a  37379  cdlemg31b0N  37380  cdlemg29  37391  cdlemg33a  37392  cdlemg36  37400  cdlemg42  37415  cdlemk16a  37542  cdlemk21-2N  37577  cdlemk32  37583  cdlemkid2  37610  cdlemk54  37644  cdlemk55a  37645  dihord10  37909
  Copyright terms: Public domain W3C validator