Theorem syl12anc 1215

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

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		sylXanc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		sylXanc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	jca32 308	. 2 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))
5		syl12anc.4	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)
6	4, 5	syl 14	1 ⊢ (𝜑 → 𝜏)

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  1218  cocan1  5696  fliftfun  5705  isopolem  5731  f1oiso2  5736  caovcld  5932  caovcomd  5935  tfrlemisucaccv  6230  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  fidceq  6771  findcard2d  6793  diffifi  6796  tridc  6801  en2eqpr  6809  sbthlemi9  6861  supisolem  6903  ordiso2  6928  difinfsnlem  6992  difinfsn  6993  prarloclemup  7327  prarloc  7335  nqprl  7383  nqpru  7384  ltaddpr  7429  aptiprlemu  7472  archpr  7475  cauappcvgprlem2  7492  caucvgprlem2  7512  caucvgprprlem2  7542  suplocexprlemlub  7556  suplocexpr  7557  recexgt0sr  7605  archsr  7614  axpre-suploclemres  7733  conjmulap  8513  lerec2  8671  ledivp1  8685  cju  8743  nn2ge  8777  gtndiv  9170  supinfneg  9417  infsupneg  9418  z2ge  9639  iccssioo2  9759  fzrev3  9898  elfz1b  9901  exbtwnzlemstep  10056  exbtwnzlemex  10058  rebtwn2zlemstep  10061  rebtwn2z  10063  qbtwnre  10065  flqdiv  10125  frec2uzled  10233  seq3caopr  10287  iseqf1olemab  10293  iseqf1olemnanb  10294  expnegzap  10358  hashen  10562  hashunlem  10582  hashprg  10586  leisorel  10612  zfz1isolemiso  10614  seq3coll  10617  caucvgrelemrec  10783  resqrexlemex  10829  minmax  11033  xrminmax  11066  fsum2dlemstep  11235  fisumcom2  11239  zproddc  11380  zsupcllemstep  11674  bezoutlemmain  11722  sqgcd  11753  neiint  12353  restbasg  12376  iscnp4  12426  cnconst2  12441  cnpdis  12450  neitx  12476  upxp  12480  hmeoimaf1o  12522  blssexps  12637  blssex  12638  ssblex  12639  bdmopn  12712  xmettx  12718  metcnp3  12719  tgioo  12754  tgqioo  12755  sin0pilem2  12911  logbgcd1irr  13092  pwle2  13366