Theorem syl21anc 1277

Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)

Hypotheses

Ref	Expression
sylXanc.1	⊢ (𝜑 → 𝜓)
sylXanc.2	⊢ (𝜑 → 𝜒)
sylXanc.3	⊢ (𝜑 → 𝜃)
syl21anc.4	⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl21anc	⊢ (𝜑 → 𝜏)

Proof of Theorem syl21anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		sylXanc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		sylXanc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	jca31 309	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))
5		syl21anc.4	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
6	4, 5	syl 14	1 ⊢ (𝜑 → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  issod  4464  brcogw  4949  funprg  5431  funtpg  5432  fnunsn  5490  fun2d  5563  ftpg  5899  fsnunf  5915  isotr  6022  off  6315  caofrss  6334  suppssfvg  6503  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  pmresg  6957  ac6sfi  7202  tridc  7204  eqsndc  7210  tpfidceq  7237  fidcenumlemrks  7270  sbthlemi8  7281  casefun  7426  caseinj  7430  djufun  7445  djuinj  7447  mulclpi  7696  archnqq  7785  addlocprlemlt  7899  addlocprlemeq  7901  addlocprlemgt  7902  mullocprlem  7938  apreim  8934  subrecap  9172  ltrec1  9221  divge0d  10149  fseq1p1m1  10512  q2submod  10836  seq3caopr2  10944  seqcaopr2g  10945  seq3distr  10983  facavg  11199  swrdwrdsymbg  11451  cats1un  11508  shftfibg  11600  sqrtdiv  11823  sqrtdivd  11950  mulcn2  12096  demoivreALT  12559  dvdslegcd  12759  gcdnncl  12762  qredeu  12893  rpdvds  12895  rpexp  12950  nnmaxpwlemnfac  12969  nnmaxpwlemparts  12970  divnumden  12994  divdenle  12995  phimullem  13025  phisum  13041  pythagtriplem4  13069  pythagtriplem8  13073  pythagtriplem9  13074  pcgcd1  13129  fldivp1  13149  pockthlem  13157  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilemfrcn0  13324  setsfun  13438  setsfun0  13439  strleund  13508  ercpbl  13703  sgrppropd  13779  mndpropd  13804  grpidssd  13932  grpinvssd  13933  issubg2m  14043  isnsg3  14061  eqgid  14080  kerf1ghm  14128  lmodprop2d  14736  lsspropdg  14819  znidomb  15044  znrrg  15046  comet  15652  fsumcncntop  15720  mulcncf  15761  zprmlogbaplem2  16138  birthdaylem3  16149  mpodvdsmulf1o  16206  gausslemma2dlem0d  16293  gausslemma2dlem1a  16299  2lgslem1a1  16327  2sqlem8a  16363  2sqlem8  16364  trilpo  17214  neapmkv  17240