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

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

Proof of Theorem syl13anc
StepHypRef Expression
1 sylXanc.1 . 2 (𝜑𝜓)
2 sylXanc.2 . . 3 (𝜑𝜒)
3 sylXanc.3 . . 3 (𝜑𝜃)
4 sylXanc.4 . . 3 (𝜑𝜏)
52, 3, 43jca 1162 . 2 (𝜑 → (𝜒𝜃𝜏))
6 syl13anc.5 . 2 ((𝜓 ∧ (𝜒𝜃𝜏)) → 𝜂)
71, 5, 6syl2anc 409 1 (𝜑𝜂)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 963 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 965 This theorem is referenced by:  syl23anc  1224  syl33anc  1232  caovassd  5970  caovcand  5973  caovordid  5977  caovordd  5979  caovdid  5986  caovdird  5989  swoer  6497  swoord1  6498  swoord2  6499  fimax2gtrilemstep  6834  iunfidisj  6879  ssfii  6907  suplub2ti  6933  prarloclem3  7396  fzosubel3  10073  seq3split  10356  seq3caopr  10360  zsumdc  11258  fsumiun  11351  divalglemex  11786  strle1g  12219  psmetsym  12668  psmettri  12669  psmetge0  12670  psmetres2  12672  xmetge0  12704  xmetsym  12707  xmettri  12711  metrtri  12716  xmetres2  12718  bldisj  12740  xblss2ps  12743  xblss2  12744  xmeter  12775  xmetxp  12846
 Copyright terms: Public domain W3C validator