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

Theorem syl12anc 1168
 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  1171  cocan1  5458  fliftfun  5467  isopolem  5492  f1oiso2  5497  caovcld  5685  caovcomd  5688  tfrlemisucaccv  5974  tfr1onlemsucaccv  5990  tfr1onlembxssdm  5992  tfrcllemsucaccv  6003  tfrcllembxssdm  6005  fidceq  6404  findcard2d  6425  diffifi  6428  en2eqpr  6434  supisolem  6480  ordiso2  6505  prarloclemup  6747  prarloc  6755  nqprl  6803  nqpru  6804  ltaddpr  6849  aptiprlemu  6892  archpr  6895  cauappcvgprlem2  6912  caucvgprlem2  6932  caucvgprprlem2  6962  recexgt0sr  7012  archsr  7020  conjmulap  7884  lerec2  8034  ledivp1  8048  cju  8105  nn2ge  8138  gtndiv  8523  supinfneg  8764  infsupneg  8765  z2ge  8969  iccssioo2  9045  fzrev3  9180  elfz1b  9183  exbtwnzlemstep  9334  exbtwnzlemex  9336  rebtwn2zlemstep  9339  rebtwn2z  9341  qbtwnre  9343  flqdiv  9403  frec2uzled  9511  iseqcaopr  9558  expnegzap  9607  sizeen  9808  sizeunlem  9828  sizeprg  9832  caucvgrelemrec  10003  resqrexlemex  10049  minmax  10250  zsupcllemstep  10485  bezoutlemmain  10531  sqgcd  10562
 Copyright terms: Public domain W3C validator