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

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

Proof of Theorem simp321
StepHypRef Expression
1 simp21 1203 . 2 ((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) → 𝜑)
213ad2ant3 1132 1 ((𝜂𝜁 ∧ (𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
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 1086
This theorem is referenced by:  dalemcnes  36891  dalempnes  36892  dalemrot  36898  dath2  36978  cdleme18d  37536  cdleme20i  37558  cdleme20j  37559  cdleme20l2  37562  cdleme20l  37563  cdleme20m  37564  cdleme20  37565  cdleme21j  37577  cdleme22eALTN  37586  cdlemk16a  38097  cdlemk12u-2N  38131  cdlemk21-2N  38132  cdlemk22  38134  cdlemk31  38137  cdlemk32  38138  cdlemk11ta  38170  cdlemk11tc  38186
  Copyright terms: Public domain W3C validator