Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  anasss GIF version

Theorem anasss 379
 Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
anasss.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
anasss ((𝜑 ∧ (𝜓𝜒)) → 𝜃)

Proof of Theorem anasss
StepHypRef Expression
1 anasss.1 . . 3 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
21exp31 346 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 244 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem is referenced by:  anass  381  anabss3  519  wepo  4096  wetrep  4097  fvun1  5239  f1elima  5412  caovimo  5694  prarloc  6601  reapmul1  7586  ltmul12a  7826  peano5uzti  8346  eluzp1m1  8496  lbzbi  8551  qreccl  8576  xrlttr  8716  xrltso  8717  elfzodifsumelfzo  9057  nn0seqcvgd  9880
 Copyright terms: Public domain W3C validator