Theorem syl12anc 1218

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  1221  cocan1  5732  fliftfun  5741  isopolem  5767  f1oiso2  5772  caovcld  5968  caovcomd  5971  tfrlemisucaccv  6266  tfr1onlemsucaccv  6282  tfr1onlembxssdm  6284  tfrcllemsucaccv  6295  tfrcllembxssdm  6297  fidceq  6807  findcard2d  6829  diffifi  6832  tridc  6837  en2eqpr  6845  sbthlemi9  6902  supisolem  6944  ordiso2  6969  difinfsnlem  7033  difinfsn  7034  prarloclemup  7398  prarloc  7406  nqprl  7454  nqpru  7455  ltaddpr  7500  aptiprlemu  7543  archpr  7546  cauappcvgprlem2  7563  caucvgprlem2  7583  caucvgprprlem2  7613  suplocexprlemlub  7627  suplocexpr  7628  recexgt0sr  7676  archsr  7685  axpre-suploclemres  7804  conjmulap  8585  lerec2  8743  ledivp1  8757  cju  8815  nn2ge  8849  gtndiv  9242  supinfneg  9489  infsupneg  9490  z2ge  9712  iccssioo2  9832  fzrev3  9971  elfz1b  9974  exbtwnzlemstep  10129  exbtwnzlemex  10131  rebtwn2zlemstep  10134  rebtwn2z  10136  qbtwnre  10138  flqdiv  10202  frec2uzled  10310  seq3caopr  10364  iseqf1olemab  10370  iseqf1olemnanb  10371  expnegzap  10435  hashen  10640  hashunlem  10660  hashprg  10664  leisorel  10690  zfz1isolemiso  10692  seq3coll  10695  caucvgrelemrec  10861  resqrexlemex  10907  minmax  11111  xrminmax  11144  fsum2dlemstep  11313  fisumcom2  11317  zproddc  11458  fprod2dlemstep  11501  fprodcom2fi  11505  zsupcllemstep  11813  bezoutlemmain  11862  sqgcd  11893  neiint  12505  restbasg  12528  iscnp4  12578  cnconst2  12593  cnpdis  12602  neitx  12628  upxp  12632  hmeoimaf1o  12674  blssexps  12789  blssex  12790  ssblex  12791  bdmopn  12864  xmettx  12870  metcnp3  12871  tgioo  12906  tgqioo  12907  sin0pilem2  13063  logbgcd1irr  13244  pwle2  13530