Theorem syl12anc 1272

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  1275  cocan1  5966  fliftfun  5975  isopolem  6001  f1oiso2  6006  caovcld  6216  caovcomd  6219  tfrlemisucaccv  6569  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  1dom1el  7073  fidceq  7137  findcard2d  7161  diffifi  7164  tridc  7170  en2eqpr  7180  sbthlemi9  7248  supisolem  7312  ordiso2  7339  difinfsnlem  7403  difinfsn  7404  pr2cv1  7505  prarloclemup  7826  prarloc  7834  nqprl  7882  nqpru  7883  ltaddpr  7928  aptiprlemu  7971  archpr  7974  cauappcvgprlem2  7991  caucvgprlem2  8011  caucvgprprlem2  8041  suplocexprlemlub  8055  suplocexpr  8056  recexgt0sr  8104  archsr  8113  axpre-suploclemres  8232  conjmulap  9023  lerec2  9183  ledivp1  9197  cju  9255  nn2ge  9290  gtndiv  9694  supinfneg  9948  infsupneg  9949  z2ge  10181  iccssioo2  10301  fzrev3  10446  elfz1b  10449  zsupcllemstep  10614  zsupssdc  10625  exbtwnzlemstep  10634  exbtwnzlemex  10636  rebtwn2zlemstep  10639  rebtwn2z  10641  qbtwnre  10643  flqdiv  10710  frec2uzled  10818  seq3caopr  10884  seqcaoprg  10885  iseqf1olemab  10891  iseqf1olemnanb  10892  seqf1oglem1  10908  expnegzap  10962  nn0ltexp2  11099  hashen  11175  hashunlem  11196  hashprg  11201  hashfibclem  11234  leisorel  11237  zfz1isolemiso  11239  seq3coll  11242  swrdccat3b  11460  caucvgrelemrec  11692  resqrexlemex  11738  minmax  11943  xrminmax  11978  fsum2dlemstep  12148  fisumcom2  12152  zproddc  12293  fprod2dlemstep  12336  fprodcom2fi  12340  bezoutlemmain  12722  sqgcd  12753  pcpremul  13019  pceulem  13020  pceu  13021  pczpre  13023  pcdiv  13028  pcqmul  13029  pcqdiv  13033  pcexp  13035  pcdvdsb  13046  pcneg  13051  pcdvdstr  13053  pcgcd1  13054  pc2dvds  13056  pcz  13058  pcaddlem  13065  pcadd  13066  qexpz  13078  expnprm  13079  infpnlem2  13086  ballotfilemfc0  13179  ballotfilemfcc  13180  f1ocpbllem  13577  f1ovscpbl  13579  sgrppropd  13679  mndpropd  13704  grpsubpropd2  13863  f1ghm0to0  14028  ablnnncan  14079  rngpropd  14197  ringpropd  14284  lmodprop2d  14625  lsspropdg  14708  neiint  15139  restbasg  15162  iscnp4  15212  cnconst2  15227  cnpdis  15236  neitx  15262  upxp  15266  hmeoimaf1o  15308  blssexps  15423  blssex  15424  ssblex  15425  bdmopn  15498  xmettx  15504  metcnp3  15505  tgioo  15548  tgqioo  15549  dvmptfsum  15719  elply2  15729  sin0pilem2  15776  logbgcd1irr  15961  perfect  15998  lgsval  16006  lgsfcl2  16008  lgsdir  16037  lgsdilem2  16038  lgsdi  16039  lgsne0  16040  clwwlknonex2e  16564  pwle2  16911  qdiff  16972