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

Theorem syl12anc 1197
Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
Hypotheses
Ref Expression
sylXanc.1 (𝜑𝜓)
sylXanc.2 (𝜑𝜒)
sylXanc.3 (𝜑𝜃)
syl12anc.4 ((𝜓 ∧ (𝜒𝜃)) → 𝜏)
Assertion
Ref Expression
syl12anc (𝜑𝜏)

Proof of Theorem syl12anc
StepHypRef Expression
1 sylXanc.1 . . 3 (𝜑𝜓)
2 sylXanc.2 . . 3 (𝜑𝜒)
3 sylXanc.3 . . 3 (𝜑𝜃)
41, 2, 3jca32 306 . 2 (𝜑 → (𝜓 ∧ (𝜒𝜃)))
5 syl12anc.4 . 2 ((𝜓 ∧ (𝜒𝜃)) → 𝜏)
64, 5syl 14 1 (𝜑𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  syl22anc  1200  cocan1  5654  fliftfun  5663  isopolem  5689  f1oiso2  5694  caovcld  5890  caovcomd  5893  tfrlemisucaccv  6188  tfr1onlemsucaccv  6204  tfr1onlembxssdm  6206  tfrcllemsucaccv  6217  tfrcllembxssdm  6219  fidceq  6729  findcard2d  6751  diffifi  6754  tridc  6759  en2eqpr  6767  sbthlemi9  6819  supisolem  6861  ordiso2  6886  difinfsnlem  6950  difinfsn  6951  prarloclemup  7267  prarloc  7275  nqprl  7323  nqpru  7324  ltaddpr  7369  aptiprlemu  7412  archpr  7415  cauappcvgprlem2  7432  caucvgprlem2  7452  caucvgprprlem2  7482  suplocexprlemlub  7496  suplocexpr  7497  recexgt0sr  7545  archsr  7554  axpre-suploclemres  7673  conjmulap  8449  lerec2  8604  ledivp1  8618  cju  8676  nn2ge  8710  gtndiv  9097  supinfneg  9339  infsupneg  9340  z2ge  9549  iccssioo2  9669  fzrev3  9807  elfz1b  9810  exbtwnzlemstep  9965  exbtwnzlemex  9967  rebtwn2zlemstep  9970  rebtwn2z  9972  qbtwnre  9974  flqdiv  10034  frec2uzled  10142  seq3caopr  10196  iseqf1olemab  10202  iseqf1olemnanb  10203  expnegzap  10267  hashen  10470  hashunlem  10490  hashprg  10494  leisorel  10520  zfz1isolemiso  10522  seq3coll  10525  caucvgrelemrec  10691  resqrexlemex  10737  minmax  10941  xrminmax  10974  fsum2dlemstep  11143  fisumcom2  11147  zsupcllemstep  11534  bezoutlemmain  11582  sqgcd  11613  neiint  12209  restbasg  12232  iscnp4  12282  cnconst2  12297  cnpdis  12306  neitx  12332  upxp  12336  hmeoimaf1o  12378  blssexps  12493  blssex  12494  ssblex  12495  bdmopn  12568  xmettx  12574  metcnp3  12575  tgioo  12610  tgqioo  12611  pwle2  12995
  Copyright terms: Public domain W3C validator