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

Theorem syl13anc 1201
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 1144 . 2 (𝜑 → (𝜒𝜃𝜏))
6 syl13anc.5 . 2 ((𝜓 ∧ (𝜒𝜃𝜏)) → 𝜂)
71, 5, 6syl2anc 406 1 (𝜑𝜂)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 945
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 947
This theorem is referenced by:  syl23anc  1206  syl33anc  1214  caovassd  5896  caovcand  5899  caovordid  5903  caovordd  5905  caovdid  5912  caovdird  5915  swoer  6423  swoord1  6424  swoord2  6425  fimax2gtrilemstep  6760  iunfidisj  6800  ssfii  6828  suplub2ti  6854  prarloclem3  7269  fzosubel3  9924  seq3split  10203  seq3caopr  10207  zsumdc  11104  fsumiun  11197  divalglemex  11526  strle1g  11955  psmetsym  12404  psmettri  12405  psmetge0  12406  psmetres2  12408  xmetge0  12440  xmetsym  12443  xmettri  12447  metrtri  12452  xmetres2  12454  bldisj  12476  xblss2ps  12479  xblss2  12480  xmeter  12511  xmetxp  12582
  Copyright terms: Public domain W3C validator