Theorem syl21anc 1215

Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)

Hypotheses

Ref	Expression
sylXanc.1	|- ( ph -> ps )
sylXanc.2	|- ( ph -> ch )
sylXanc.3	|- ( ph -> th )
syl21anc.4	|- ( ( ( ps /\ ch ) /\ th ) -> ta )

Assertion

Ref	Expression
syl21anc	|- ( ph -> ta )

Proof of Theorem syl21anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 |- ( ph -> ps )
2		sylXanc.2	. . 3 |- ( ph -> ch )
3		sylXanc.3	. . 3 |- ( ph -> th )
4	1, 2, 3	jca31 307	. 2 |- ( ph -> ( ( ps /\ ch ) /\ th ) )
5		syl21anc.4	. 2 |- ( ( ( ps /\ ch ) /\ th ) -> ta )
6	4, 5	syl 14	1 |- ( ph -> ta )

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  4236  brcogw  4703  funprg  5168  funtpg  5169  fnunsn  5225  ftpg  5597  fsnunf  5613  isotr  5710  off  5987  caofrss  5999  tfr1onlembxssdm  6233  tfrcllembxssdm  6246  pmresg  6563  ac6sfi  6785  tridc  6786  fidcenumlemrks  6834  sbthlemi8  6845  casefun  6963  caseinj  6967  djufun  6982  djuinj  6984  mulclpi  7129  archnqq  7218  addlocprlemlt  7332  addlocprlemeq  7334  addlocprlemgt  7335  mullocprlem  7371  apreim  8358  subrecap  8591  ltrec1  8639  divge0d  9517  fseq1p1m1  9867  q2submod  10151  seq3caopr2  10248  seq3distr  10279  facavg  10485  shftfibg  10585  sqrtdiv  10807  sqrtdivd  10933  mulcn2  11074  demoivreALT  11469  dvdslegcd  11642  gcdnncl  11645  qredeu  11767  rpdvds  11769  rpexp  11820  oddpwdclemodd  11839  divnumden  11863  divdenle  11864  phimullem  11890  setsfun  11983  setsfun0  11984  strleund  12036  comet  12657  fsumcncntop  12714  mulcncf  12749  trilpo  13225