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  5788  fliftfun  5797  isopolem  5823  f1oiso2  5828  caovcld  6028  caovcomd  6031  tfrlemisucaccv  6326  tfr1onlemsucaccv  6342  tfr1onlembxssdm  6344  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  fidceq  6869  findcard2d  6891  diffifi  6894  tridc  6899  en2eqpr  6907  sbthlemi9  6964  supisolem  7007  ordiso2  7034  difinfsnlem  7098  difinfsn  7099  prarloclemup  7494  prarloc  7502  nqprl  7550  nqpru  7551  ltaddpr  7596  aptiprlemu  7639  archpr  7642  cauappcvgprlem2  7659  caucvgprlem2  7679  caucvgprprlem2  7709  suplocexprlemlub  7723  suplocexpr  7724  recexgt0sr  7772  archsr  7781  axpre-suploclemres  7900  conjmulap  8686  lerec2  8846  ledivp1  8860  cju  8918  nn2ge  8952  gtndiv  9348  supinfneg  9595  infsupneg  9596  z2ge  9826  iccssioo2  9946  fzrev3  10087  elfz1b  10090  exbtwnzlemstep  10248  exbtwnzlemex  10250  rebtwn2zlemstep  10253  rebtwn2z  10255  qbtwnre  10257  flqdiv  10321  frec2uzled  10429  seq3caopr  10483  iseqf1olemab  10489  iseqf1olemnanb  10490  expnegzap  10554  nn0ltexp2  10689  hashen  10764  hashunlem  10784  hashprg  10788  leisorel  10817  zfz1isolemiso  10819  seq3coll  10822  caucvgrelemrec  10988  resqrexlemex  11034  minmax  11238  xrminmax  11273  fsum2dlemstep  11442  fisumcom2  11446  zproddc  11587  fprod2dlemstep  11630  fprodcom2fi  11634  zsupcllemstep  11946  zsupssdc  11955  bezoutlemmain  11999  sqgcd  12030  pcpremul  12293  pceulem  12294  pceu  12295  pczpre  12297  pcdiv  12302  pcqmul  12303  pcqdiv  12307  pcexp  12309  pcdvdsb  12319  pcneg  12324  pcdvdstr  12326  pcgcd1  12327  pc2dvds  12329  pcz  12331  pcaddlem  12338  pcadd  12339  qexpz  12350  expnprm  12351  infpnlem2  12358  f1ocpbllem  12731  f1ovscpbl  12733  mndpropd  12841  grpsubpropd2  12975  ablnnncan  13126  ringpropd  13217  lmodprop2d  13438  neiint  13648  restbasg  13671  iscnp4  13721  cnconst2  13736  cnpdis  13745  neitx  13771  upxp  13775  hmeoimaf1o  13817  blssexps  13932  blssex  13933  ssblex  13934  bdmopn  14007  xmettx  14013  metcnp3  14014  tgioo  14049  tgqioo  14050  sin0pilem2  14206  logbgcd1irr  14388  lgsval  14408  lgsfcl2  14410  lgsdir  14439  lgsdilem2  14440  lgsdi  14441  lgsne0  14442  pwle2  14751