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

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

Proof of Theorem simp132
StepHypRef Expression
1 simp32 1211 . 2 ((𝜃𝜏 ∧ (𝜑𝜓𝜒)) → 𝜓)
213ad2ant1 1134 1 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂𝜁) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  ax5seglem3  28169  3atlem1  38292  3atlem2  38293  3atlem5  38296  2llnjaN  38375  4atlem11b  38417  4atlem12b  38420  lplncvrlvol2  38424  dalemtea  38439  dath2  38546  cdlemblem  38602  dalawlem1  38680  lhpexle3lem  38820  4atexlemex6  38883  cdleme22f2  39156  cdleme22g  39157  cdlemg7aN  39434  cdlemg34  39521  cdlemj1  39630  cdlemk23-3  39711  cdlemk25-3  39713  cdlemk26b-3  39714
  Copyright terms: Public domain W3C validator