Theorem syl12anc 1236

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 310	. 2 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))
5		syl12anc.4	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)
6	4, 5	syl 14	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  syl22anc  1239  cocan1  5783  fliftfun  5792  isopolem  5818  f1oiso2  5823  caovcld  6023  caovcomd  6026  tfrlemisucaccv  6321  tfr1onlemsucaccv  6337  tfr1onlembxssdm  6339  tfrcllemsucaccv  6350  tfrcllembxssdm  6352  fidceq  6864  findcard2d  6886  diffifi  6889  tridc  6894  en2eqpr  6902  sbthlemi9  6959  supisolem  7002  ordiso2  7029  difinfsnlem  7093  difinfsn  7094  prarloclemup  7489  prarloc  7497  nqprl  7545  nqpru  7546  ltaddpr  7591  aptiprlemu  7634  archpr  7637  cauappcvgprlem2  7654  caucvgprlem2  7674  caucvgprprlem2  7704  suplocexprlemlub  7718  suplocexpr  7719  recexgt0sr  7767  archsr  7776  axpre-suploclemres  7895  conjmulap  8680  lerec2  8840  ledivp1  8854  cju  8912  nn2ge  8946  gtndiv  9342  supinfneg  9589  infsupneg  9590  z2ge  9820  iccssioo2  9940  fzrev3  10080  elfz1b  10083  exbtwnzlemstep  10241  exbtwnzlemex  10243  rebtwn2zlemstep  10246  rebtwn2z  10248  qbtwnre  10250  flqdiv  10314  frec2uzled  10422  seq3caopr  10476  iseqf1olemab  10482  iseqf1olemnanb  10483  expnegzap  10547  nn0ltexp2  10681  hashen  10755  hashunlem  10775  hashprg  10779  leisorel  10808  zfz1isolemiso  10810  seq3coll  10813  caucvgrelemrec  10979  resqrexlemex  11025  minmax  11229  xrminmax  11264  fsum2dlemstep  11433  fisumcom2  11437  zproddc  11578  fprod2dlemstep  11621  fprodcom2fi  11625  zsupcllemstep  11936  zsupssdc  11945  bezoutlemmain  11989  sqgcd  12020  pcpremul  12283  pceulem  12284  pceu  12285  pczpre  12287  pcdiv  12292  pcqmul  12293  pcqdiv  12297  pcexp  12299  pcdvdsb  12309  pcneg  12314  pcdvdstr  12316  pcgcd1  12317  pc2dvds  12319  pcz  12321  pcaddlem  12328  pcadd  12329  qexpz  12340  expnprm  12341  infpnlem2  12348  mndpropd  12771  grpsubpropd2  12903  ablnnncan  13026  ringpropd  13117  neiint  13427  restbasg  13450  iscnp4  13500  cnconst2  13515  cnpdis  13524  neitx  13550  upxp  13554  hmeoimaf1o  13596  blssexps  13711  blssex  13712  ssblex  13713  bdmopn  13786  xmettx  13792  metcnp3  13793  tgioo  13828  tgqioo  13829  sin0pilem2  13985  logbgcd1irr  14167  lgsval  14187  lgsfcl2  14189  lgsdir  14218  lgsdilem2  14219  lgsdi  14220  lgsne0  14221  pwle2  14519