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  5959  fliftfun  5968  isopolem  5994  f1oiso2  5999  caovcld  6207  caovcomd  6210  tfrlemisucaccv  6555  tfr1onlemsucaccv  6571  tfr1onlembxssdm  6573  tfrcllemsucaccv  6584  tfrcllembxssdm  6586  1dom1el  7059  fidceq  7123  findcard2d  7147  diffifi  7150  tridc  7156  en2eqpr  7166  sbthlemi9  7234  supisolem  7298  ordiso2  7325  difinfsnlem  7389  difinfsn  7390  pr2cv1  7491  prarloclemup  7806  prarloc  7814  nqprl  7862  nqpru  7863  ltaddpr  7908  aptiprlemu  7951  archpr  7954  cauappcvgprlem2  7971  caucvgprlem2  7991  caucvgprprlem2  8021  suplocexprlemlub  8035  suplocexpr  8036  recexgt0sr  8084  archsr  8093  axpre-suploclemres  8212  conjmulap  8999  lerec2  9159  ledivp1  9173  cju  9231  nn2ge  9266  gtndiv  9669  supinfneg  9923  infsupneg  9924  z2ge  10155  iccssioo2  10275  fzrev3  10417  elfz1b  10420  zsupcllemstep  10585  zsupssdc  10594  exbtwnzlemstep  10603  exbtwnzlemex  10605  rebtwn2zlemstep  10608  rebtwn2z  10610  qbtwnre  10612  flqdiv  10679  frec2uzled  10787  seq3caopr  10853  seqcaoprg  10854  iseqf1olemab  10860  iseqf1olemnanb  10861  seqf1oglem1  10877  expnegzap  10931  nn0ltexp2  11067  hashen  11142  hashunlem  11163  hashprg  11168  hashfibclem  11199  leisorel  11202  zfz1isolemiso  11204  seq3coll  11207  swrdccat3b  11425  caucvgrelemrec  11657  resqrexlemex  11703  minmax  11908  xrminmax  11943  fsum2dlemstep  12113  fisumcom2  12117  zproddc  12258  fprod2dlemstep  12301  fprodcom2fi  12305  bezoutlemmain  12687  sqgcd  12718  pcpremul  12984  pceulem  12985  pceu  12986  pczpre  12988  pcdiv  12993  pcqmul  12994  pcqdiv  12998  pcexp  13000  pcdvdsb  13011  pcneg  13016  pcdvdstr  13018  pcgcd1  13019  pc2dvds  13021  pcz  13023  pcaddlem  13030  pcadd  13031  qexpz  13043  expnprm  13044  infpnlem2  13051  f1ocpbllem  13512  f1ovscpbl  13514  sgrppropd  13615  mndpropd  13642  grpsubpropd2  13807  f1ghm0to0  13978  ablnnncan  14029  rngpropd  14088  ringpropd  14171  lmodprop2d  14483  lsspropdg  14566  neiint  14997  restbasg  15020  iscnp4  15070  cnconst2  15085  cnpdis  15094  neitx  15120  upxp  15124  hmeoimaf1o  15166  blssexps  15281  blssex  15282  ssblex  15283  bdmopn  15356  xmettx  15362  metcnp3  15363  tgioo  15406  tgqioo  15407  dvmptfsum  15577  elply2  15587  sin0pilem2  15634  logbgcd1irr  15819  perfect  15856  lgsval  15864  lgsfcl2  15866  lgsdir  15895  lgsdilem2  15896  lgsdi  15897  lgsne0  15898  clwwlknonex2e  16422  pwle2  16759  qdiff  16820