Theorem syl12anc 1248

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  1251  cocan1  5863  fliftfun  5872  isopolem  5898  f1oiso2  5903  caovcld  6107  caovcomd  6110  tfrlemisucaccv  6418  tfr1onlemsucaccv  6434  tfr1onlembxssdm  6436  tfrcllemsucaccv  6447  tfrcllembxssdm  6449  fidceq  6973  findcard2d  6995  diffifi  6998  tridc  7003  en2eqpr  7011  sbthlemi9  7074  supisolem  7117  ordiso2  7144  difinfsnlem  7208  difinfsn  7209  prarloclemup  7615  prarloc  7623  nqprl  7671  nqpru  7672  ltaddpr  7717  aptiprlemu  7760  archpr  7763  cauappcvgprlem2  7780  caucvgprlem2  7800  caucvgprprlem2  7830  suplocexprlemlub  7844  suplocexpr  7845  recexgt0sr  7893  archsr  7902  axpre-suploclemres  8021  conjmulap  8809  lerec2  8969  ledivp1  8983  cju  9041  nn2ge  9076  gtndiv  9475  supinfneg  9723  infsupneg  9724  z2ge  9955  iccssioo2  10075  fzrev3  10216  elfz1b  10219  zsupcllemstep  10379  zsupssdc  10388  exbtwnzlemstep  10397  exbtwnzlemex  10399  rebtwn2zlemstep  10402  rebtwn2z  10404  qbtwnre  10406  flqdiv  10473  frec2uzled  10581  seq3caopr  10647  seqcaoprg  10648  iseqf1olemab  10654  iseqf1olemnanb  10655  seqf1oglem1  10671  expnegzap  10725  nn0ltexp2  10861  hashen  10936  hashunlem  10956  hashprg  10960  leisorel  10989  zfz1isolemiso  10991  seq3coll  10994  caucvgrelemrec  11334  resqrexlemex  11380  minmax  11585  xrminmax  11620  fsum2dlemstep  11789  fisumcom2  11793  zproddc  11934  fprod2dlemstep  11977  fprodcom2fi  11981  bezoutlemmain  12363  sqgcd  12394  pcpremul  12660  pceulem  12661  pceu  12662  pczpre  12664  pcdiv  12669  pcqmul  12670  pcqdiv  12674  pcexp  12676  pcdvdsb  12687  pcneg  12692  pcdvdstr  12694  pcgcd1  12695  pc2dvds  12697  pcz  12699  pcaddlem  12706  pcadd  12707  qexpz  12719  expnprm  12720  infpnlem2  12727  f1ocpbllem  13186  f1ovscpbl  13188  sgrppropd  13289  mndpropd  13316  grpsubpropd2  13481  f1ghm0to0  13652  ablnnncan  13703  rngpropd  13761  ringpropd  13844  lmodprop2d  14154  lsspropdg  14237  neiint  14661  restbasg  14684  iscnp4  14734  cnconst2  14749  cnpdis  14758  neitx  14784  upxp  14788  hmeoimaf1o  14830  blssexps  14945  blssex  14946  ssblex  14947  bdmopn  15020  xmettx  15026  metcnp3  15027  tgioo  15070  tgqioo  15071  dvmptfsum  15241  elply2  15251  sin0pilem2  15298  logbgcd1irr  15483  perfect  15517  lgsval  15525  lgsfcl2  15527  lgsdir  15556  lgsdilem2  15557  lgsdi  15558  lgsne0  15559  1dom1el  16001  pwle2  16009