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

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

Proof of Theorem syl21anc
StepHypRef Expression
1 sylXanc.1 . . 3 (𝜑𝜓)
2 sylXanc.2 . . 3 (𝜑𝜒)
3 sylXanc.3 . . 3 (𝜑𝜃)
41, 2, 3jca31 307 . 2 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
5 syl21anc.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:  issod  4244  brcogw  4711  funprg  5176  funtpg  5177  fnunsn  5233  ftpg  5607  fsnunf  5623  isotr  5720  off  5997  caofrss  6009  tfr1onlembxssdm  6243  tfrcllembxssdm  6256  pmresg  6573  ac6sfi  6795  tridc  6796  fidcenumlemrks  6844  sbthlemi8  6855  casefun  6973  caseinj  6977  djufun  6992  djuinj  6994  mulclpi  7155  archnqq  7244  addlocprlemlt  7358  addlocprlemeq  7360  addlocprlemgt  7361  mullocprlem  7397  apreim  8384  subrecap  8617  ltrec1  8665  divge0d  9547  fseq1p1m1  9898  q2submod  10182  seq3caopr2  10279  seq3distr  10310  facavg  10516  shftfibg  10616  sqrtdiv  10838  sqrtdivd  10964  mulcn2  11105  demoivreALT  11503  dvdslegcd  11676  gcdnncl  11679  qredeu  11801  rpdvds  11803  rpexp  11854  oddpwdclemodd  11873  divnumden  11897  divdenle  11898  phimullem  11924  setsfun  12020  setsfun0  12021  strleund  12073  comet  12694  fsumcncntop  12751  mulcncf  12786  trilpo  13384  neapmkv  13398
 Copyright terms: Public domain W3C validator