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  5962  fliftfun  5971  isopolem  5997  f1oiso2  6002  caovcld  6210  caovcomd  6213  tfrlemisucaccv  6558  tfr1onlemsucaccv  6574  tfr1onlembxssdm  6576  tfrcllemsucaccv  6587  tfrcllembxssdm  6589  1dom1el  7062  fidceq  7126  findcard2d  7150  diffifi  7153  tridc  7159  en2eqpr  7169  sbthlemi9  7237  supisolem  7301  ordiso2  7328  difinfsnlem  7392  difinfsn  7393  pr2cv1  7494  prarloclemup  7815  prarloc  7823  nqprl  7871  nqpru  7872  ltaddpr  7917  aptiprlemu  7960  archpr  7963  cauappcvgprlem2  7980  caucvgprlem2  8000  caucvgprprlem2  8030  suplocexprlemlub  8044  suplocexpr  8045  recexgt0sr  8093  archsr  8102  axpre-suploclemres  8221  conjmulap  9008  lerec2  9168  ledivp1  9182  cju  9240  nn2ge  9275  gtndiv  9679  supinfneg  9933  infsupneg  9934  z2ge  10165  iccssioo2  10285  fzrev3  10428  elfz1b  10431  zsupcllemstep  10596  zsupssdc  10605  exbtwnzlemstep  10614  exbtwnzlemex  10616  rebtwn2zlemstep  10619  rebtwn2z  10621  qbtwnre  10623  flqdiv  10690  frec2uzled  10798  seq3caopr  10864  seqcaoprg  10865  iseqf1olemab  10871  iseqf1olemnanb  10872  seqf1oglem1  10888  expnegzap  10942  nn0ltexp2  11079  hashen  11155  hashunlem  11176  hashprg  11181  hashfibclem  11214  leisorel  11217  zfz1isolemiso  11219  seq3coll  11222  swrdccat3b  11440  caucvgrelemrec  11672  resqrexlemex  11718  minmax  11923  xrminmax  11958  fsum2dlemstep  12128  fisumcom2  12132  zproddc  12273  fprod2dlemstep  12316  fprodcom2fi  12320  bezoutlemmain  12702  sqgcd  12733  pcpremul  12999  pceulem  13000  pceu  13001  pczpre  13003  pcdiv  13008  pcqmul  13009  pcqdiv  13013  pcexp  13015  pcdvdsb  13026  pcneg  13031  pcdvdstr  13033  pcgcd1  13034  pc2dvds  13036  pcz  13038  pcaddlem  13045  pcadd  13046  qexpz  13058  expnprm  13059  infpnlem2  13066  ballotfilemfc0  13157  ballotfilemfcc  13158  f1ocpbllem  13544  f1ovscpbl  13546  sgrppropd  13647  mndpropd  13674  grpsubpropd2  13839  f1ghm0to0  14010  ablnnncan  14061  rngpropd  14120  ringpropd  14203  lmodprop2d  14545  lsspropdg  14628  neiint  15059  restbasg  15082  iscnp4  15132  cnconst2  15147  cnpdis  15156  neitx  15182  upxp  15186  hmeoimaf1o  15228  blssexps  15343  blssex  15344  ssblex  15345  bdmopn  15418  xmettx  15424  metcnp3  15425  tgioo  15468  tgqioo  15469  dvmptfsum  15639  elply2  15649  sin0pilem2  15696  logbgcd1irr  15881  perfect  15918  lgsval  15926  lgsfcl2  15928  lgsdir  15957  lgsdilem2  15958  lgsdi  15959  lgsne0  15960  clwwlknonex2e  16484  pwle2  16821  qdiff  16882