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

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

Proof of Theorem syl122anc
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 syl122anc.6 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
81, 2, 3, 6, 7syl121anc 1243 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:  divdiv32apd  8772  divcanap5d  8773  divcanap7d  8775  divdivap1d  8778  divdivap2d  8779  seq3coll  10821  cau3lem  11122  summodclem2a  11388  prodmodclem2a  11583  prmind2  12119  divnumden  12195  pceulem  12293  pcqmul  12302  pcqdiv  12306  pcexp  12308  pcaddlem  12337  pcbc  12348  abladdsub4  13115  ablpnpcan  13121  lmodvs1  13404  blss2ps  13876  blss2  13877  blssps  13897  blss  13898  xmeter  13906  lgsdi  14408
  Copyright terms: Public domain W3C validator