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

Theorem syl12anc 1133
 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 293 . 2 (𝜑 → (𝜓 ∧ (𝜒𝜃)))
5 syl12anc.4 . 2 ((𝜓 ∧ (𝜒𝜃)) → 𝜏)
64, 5syl 14 1 (𝜑𝜏)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101 This theorem is referenced by:  syl22anc  1136  cocan1  5427  fliftfun  5436  isopolem  5461  f1oiso2  5466  caovcld  5654  caovcomd  5657  tfrlemisucaccv  5939  fidceq  6330  findcard2d  6348  diffifi  6351  ordiso2  6357  prarloclemup  6593  prarloc  6601  nqprl  6649  nqpru  6650  ltaddpr  6695  aptiprlemu  6738  archpr  6741  cauappcvgprlem2  6758  caucvgprlem2  6778  caucvgprprlem2  6808  recexgt0sr  6858  archsr  6866  conjmulap  7705  lerec2  7855  ledivp1  7869  cju  7913  nn2ge  7946  gtndiv  8335  z2ge  8739  iccssioo2  8815  fzrev3  8949  elfz1b  8952  qbtwnzlemstep  9103  qbtwnzlemex  9105  rebtwn2zlemstep  9107  rebtwn2z  9109  qbtwnre  9111  flqdiv  9163  iseqcaopr  9242  expnegzap  9289  caucvgrelemrec  9578  resqrexlemex  9623
 Copyright terms: Public domain W3C validator