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  8749  divcanap5d  8750  divcanap7d  8752  divdivap1d  8755  divdivap2d  8756  seq3coll  10793  cau3lem  11094  summodclem2a  11360  prodmodclem2a  11555  prmind2  12090  divnumden  12166  pceulem  12264  pcqmul  12273  pcqdiv  12277  pcexp  12279  pcaddlem  12308  pcbc  12319  abladdsub4  12931  ablpnpcan  12937  blss2ps  13539  blss2  13540  blssps  13560  blss  13561  xmeter  13569  lgsdi  14071
  Copyright terms: Public domain W3C validator