Theorem syl12anc 1214

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 )
syl12anc.4	|- ( ( ps /\ ( ch /\ th ) ) -> ta )

Assertion

Ref	Expression
syl12anc	|- ( ph -> ta )

Proof of Theorem syl12anc

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	jca32 308	. 2 |- ( ph -> ( ps /\ ( ch /\ th ) ) )
5		syl12anc.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:  syl22anc  1217  cocan1  5681  fliftfun  5690  isopolem  5716  f1oiso2  5721  caovcld  5917  caovcomd  5920  tfrlemisucaccv  6215  tfr1onlemsucaccv  6231  tfr1onlembxssdm  6233  tfrcllemsucaccv  6244  tfrcllembxssdm  6246  fidceq  6756  findcard2d  6778  diffifi  6781  tridc  6786  en2eqpr  6794  sbthlemi9  6846  supisolem  6888  ordiso2  6913  difinfsnlem  6977  difinfsn  6978  prarloclemup  7296  prarloc  7304  nqprl  7352  nqpru  7353  ltaddpr  7398  aptiprlemu  7441  archpr  7444  cauappcvgprlem2  7461  caucvgprlem2  7481  caucvgprprlem2  7511  suplocexprlemlub  7525  suplocexpr  7526  recexgt0sr  7574  archsr  7583  axpre-suploclemres  7702  conjmulap  8482  lerec2  8640  ledivp1  8654  cju  8712  nn2ge  8746  gtndiv  9139  supinfneg  9383  infsupneg  9384  z2ge  9602  iccssioo2  9722  fzrev3  9860  elfz1b  9863  exbtwnzlemstep  10018  exbtwnzlemex  10020  rebtwn2zlemstep  10023  rebtwn2z  10025  qbtwnre  10027  flqdiv  10087  frec2uzled  10195  seq3caopr  10249  iseqf1olemab  10255  iseqf1olemnanb  10256  expnegzap  10320  hashen  10523  hashunlem  10543  hashprg  10547  leisorel  10573  zfz1isolemiso  10575  seq3coll  10578  caucvgrelemrec  10744  resqrexlemex  10790  minmax  10994  xrminmax  11027  fsum2dlemstep  11196  fisumcom2  11200  zsupcllemstep  11627  bezoutlemmain  11675  sqgcd  11706  neiint  12303  restbasg  12326  iscnp4  12376  cnconst2  12391  cnpdis  12400  neitx  12426  upxp  12430  hmeoimaf1o  12472  blssexps  12587  blssex  12588  ssblex  12589  bdmopn  12662  xmettx  12668  metcnp3  12669  tgioo  12704  tgqioo  12705  sin0pilem2  12852  pwle2  13182