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

Theorem syl12anc 1170
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 303 . 2 (𝜑 → (𝜓 ∧ (𝜒𝜃)))
5 syl12anc.4 . 2 ((𝜓 ∧ (𝜒𝜃)) → 𝜏)
64, 5syl 14 1 (𝜑𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  syl22anc  1173  cocan1  5529  fliftfun  5538  isopolem  5564  f1oiso2  5569  caovcld  5757  caovcomd  5760  tfrlemisucaccv  6046  tfr1onlemsucaccv  6062  tfr1onlembxssdm  6064  tfrcllemsucaccv  6075  tfrcllembxssdm  6077  fidceq  6539  findcard2d  6561  diffifi  6564  tridc  6569  en2eqpr  6577  sbthlemi9  6621  supisolem  6650  ordiso2  6675  prarloclemup  7001  prarloc  7009  nqprl  7057  nqpru  7058  ltaddpr  7103  aptiprlemu  7146  archpr  7149  cauappcvgprlem2  7166  caucvgprlem2  7186  caucvgprprlem2  7216  recexgt0sr  7266  archsr  7274  conjmulap  8138  lerec2  8288  ledivp1  8302  cju  8359  nn2ge  8392  gtndiv  8777  supinfneg  9018  infsupneg  9019  z2ge  9223  iccssioo2  9299  fzrev3  9434  elfz1b  9437  exbtwnzlemstep  9590  exbtwnzlemex  9592  rebtwn2zlemstep  9595  rebtwn2z  9597  qbtwnre  9599  flqdiv  9659  frec2uzled  9767  iseqcaopr  9820  iseqf1olemab  9826  iseqf1olemnanb  9827  expnegzap  9891  hashen  10092  hashunlem  10112  hashprg  10116  leisorel  10142  zfz1isolemiso  10144  iseqcoll  10147  caucvgrelemrec  10311  resqrexlemex  10357  minmax  10559  zsupcllemstep  10847  bezoutlemmain  10893  sqgcd  10924
  Copyright terms: Public domain W3C validator