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

Theorem syl122anc 1259
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 1255 1 (𝜑𝜁)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 981
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 983
This theorem is referenced by:  divdiv32apd  8896  divcanap5d  8897  divcanap7d  8899  divdivap1d  8902  divdivap2d  8903  seq3coll  10994  cau3lem  11469  summodclem2a  11736  prodmodclem2a  11931  prmind2  12486  divnumden  12562  pceulem  12661  pcqmul  12670  pcqdiv  12674  pcexp  12676  pcaddlem  12706  pcbc  12718  abladdsub4  13694  ablpnpcan  13700  lmodvs1  14122  blss2ps  14922  blss2  14923  blssps  14943  blss  14944  xmeter  14952  lgsdi  15558
  Copyright terms: Public domain W3C validator