Theorem syl21anc 1216

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  4249  brcogw  4716  funprg  5181  funtpg  5182  fnunsn  5238  ftpg  5612  fsnunf  5628  isotr  5725  off  6002  caofrss  6014  tfr1onlembxssdm  6248  tfrcllembxssdm  6261  pmresg  6578  ac6sfi  6800  tridc  6801  fidcenumlemrks  6849  sbthlemi8  6860  casefun  6978  caseinj  6982  djufun  6997  djuinj  6999  mulclpi  7160  archnqq  7249  addlocprlemlt  7363  addlocprlemeq  7365  addlocprlemgt  7366  mullocprlem  7402  apreim  8389  subrecap  8622  ltrec1  8670  divge0d  9554  fseq1p1m1  9905  q2submod  10189  seq3caopr2  10286  seq3distr  10317  facavg  10524  shftfibg  10624  sqrtdiv  10846  sqrtdivd  10972  mulcn2  11113  demoivreALT  11516  dvdslegcd  11689  gcdnncl  11692  qredeu  11814  rpdvds  11816  rpexp  11867  oddpwdclemodd  11886  divnumden  11910  divdenle  11911  phimullem  11937  setsfun  12033  setsfun0  12034  strleund  12086  comet  12707  fsumcncntop  12764  mulcncf  12799  trilpo  13411  neapmkv  13425