Theorem syl12anc 1271

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  1274  cocan1  5930  fliftfun  5939  isopolem  5965  f1oiso2  5970  caovcld  6178  caovcomd  6181  tfrlemisucaccv  6493  tfr1onlemsucaccv  6509  tfr1onlembxssdm  6511  tfrcllemsucaccv  6522  tfrcllembxssdm  6524  1dom1el  6995  fidceq  7058  findcard2d  7082  diffifi  7085  tridc  7091  en2eqpr  7101  sbthlemi9  7166  supisolem  7209  ordiso2  7236  difinfsnlem  7300  difinfsn  7301  pr2cv1  7402  prarloclemup  7717  prarloc  7725  nqprl  7773  nqpru  7774  ltaddpr  7819  aptiprlemu  7862  archpr  7865  cauappcvgprlem2  7882  caucvgprlem2  7902  caucvgprprlem2  7932  suplocexprlemlub  7946  suplocexpr  7947  recexgt0sr  7995  archsr  8004  axpre-suploclemres  8123  conjmulap  8911  lerec2  9071  ledivp1  9085  cju  9143  nn2ge  9178  gtndiv  9577  supinfneg  9831  infsupneg  9832  z2ge  10063  iccssioo2  10183  fzrev3  10324  elfz1b  10327  zsupcllemstep  10492  zsupssdc  10501  exbtwnzlemstep  10510  exbtwnzlemex  10512  rebtwn2zlemstep  10515  rebtwn2z  10517  qbtwnre  10519  flqdiv  10586  frec2uzled  10694  seq3caopr  10760  seqcaoprg  10761  iseqf1olemab  10767  iseqf1olemnanb  10768  seqf1oglem1  10784  expnegzap  10838  nn0ltexp2  10974  hashen  11049  hashunlem  11070  hashprg  11075  leisorel  11104  zfz1isolemiso  11106  seq3coll  11109  swrdccat3b  11327  caucvgrelemrec  11559  resqrexlemex  11605  minmax  11810  xrminmax  11845  fsum2dlemstep  12015  fisumcom2  12019  zproddc  12160  fprod2dlemstep  12203  fprodcom2fi  12207  bezoutlemmain  12589  sqgcd  12620  pcpremul  12886  pceulem  12887  pceu  12888  pczpre  12890  pcdiv  12895  pcqmul  12896  pcqdiv  12900  pcexp  12902  pcdvdsb  12913  pcneg  12918  pcdvdstr  12920  pcgcd1  12921  pc2dvds  12923  pcz  12925  pcaddlem  12932  pcadd  12933  qexpz  12945  expnprm  12946  infpnlem2  12953  f1ocpbllem  13413  f1ovscpbl  13415  sgrppropd  13516  mndpropd  13543  grpsubpropd2  13708  f1ghm0to0  13879  ablnnncan  13930  rngpropd  13989  ringpropd  14072  lmodprop2d  14383  lsspropdg  14466  neiint  14895  restbasg  14918  iscnp4  14968  cnconst2  14983  cnpdis  14992  neitx  15018  upxp  15022  hmeoimaf1o  15064  blssexps  15179  blssex  15180  ssblex  15181  bdmopn  15254  xmettx  15260  metcnp3  15261  tgioo  15304  tgqioo  15305  dvmptfsum  15475  elply2  15485  sin0pilem2  15532  logbgcd1irr  15717  perfect  15751  lgsval  15759  lgsfcl2  15761  lgsdir  15790  lgsdilem2  15791  lgsdi  15792  lgsne0  15793  clwwlknonex2e  16317  pwle2  16657  qdiff  16715