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

Theorem syl122anc 1237
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 304 . 2 (𝜑 → (𝜏𝜂))
7 syl122anc.6 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
81, 2, 3, 6, 7syl121anc 1233 1 (𝜑𝜁)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 970
This theorem is referenced by:  divdiv32apd  8712  divcanap5d  8713  divcanap7d  8715  divdivap1d  8718  divdivap2d  8719  seq3coll  10755  cau3lem  11056  summodclem2a  11322  prodmodclem2a  11517  prmind2  12052  divnumden  12128  pceulem  12226  pcqmul  12235  pcqdiv  12239  pcexp  12241  pcaddlem  12270  pcbc  12281  blss2ps  13046  blss2  13047  blssps  13067  blss  13068  xmeter  13076  lgsdi  13578
  Copyright terms: Public domain W3C validator