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

Theorem syl32anc 1246
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1 (𝜑𝜓)
sylXanc.2 (𝜑𝜒)
sylXanc.3 (𝜑𝜃)
sylXanc.4 (𝜑𝜏)
sylXanc.5 (𝜑𝜂)
syl32anc.6 (((𝜓𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
Assertion
Ref Expression
syl32anc (𝜑𝜁)

Proof of Theorem syl32anc
StepHypRef Expression
1 sylXanc.1 . 2 (𝜑𝜓)
2 sylXanc.2 . 2 (𝜑𝜒)
3 sylXanc.3 . 2 (𝜑𝜃)
4 sylXanc.4 . . 3 (𝜑𝜏)
5 sylXanc.5 . . 3 (𝜑𝜂)
64, 5jca 306 . 2 (𝜑 → (𝜏𝜂))
7 syl32anc.6 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
81, 2, 3, 6, 7syl31anc 1241 1 (𝜑𝜁)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  ioom  10261  modifeq2int  10386  modaddmodup  10387  seq3f1olemqsum  10500  seq3f1o  10504  exple1  10576  leexp2rd  10684  nn0ltexp2  10689  facubnd  10725  permnn  10751  dfabsmax  11226  expcnvre  11511  dvdsadd2b  11847  dvdsmulgcd  12026  sqgcd  12030  bezoutr  12033  cncongr2  12104  pw2dvds  12166  hashgcdlem  12238  modprm0  12254  modprmn0modprm0  12256  tgioo  14049  lgssq  14444  lgssq2  14445
  Copyright terms: Public domain W3C validator