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  7425  caseinj  7429  djufun  7444  djuinj  7446  mulclpi  7695  archnqq  7784  addlocprlemlt  7898  addlocprlemeq  7900  addlocprlemgt  7901  mullocprlem  7937  apreim  8932  subrecap  9170  ltrec1  9219  divge0d  10140  fseq1p1m1  10503  q2submod  10824  seq3caopr2  10932  seqcaopr2g  10933  seq3distr  10971  facavg  11186  swrdwrdsymbg  11438  cats1un  11495  shftfibg  11587  sqrtdiv  11810  sqrtdivd  11936  mulcn2  12080  demoivreALT  12543  dvdslegcd  12743  gcdnncl  12746  qredeu  12877  rpdvds  12879  rpexp  12933  oddpwdclemodd  12952  divnumden  12976  divdenle  12977  phimullem  13005  phisum  13021  pythagtriplem4  13049  pythagtriplem8  13053  pythagtriplem9  13054  pcgcd1  13109  fldivp1  13129  pockthlem  13137  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemfrcn0  13275  setsfun  13389  setsfun0  13390  strleund  13459  ercpbl  13654  sgrppropd  13730  mndpropd  13755  grpidssd  13883  grpinvssd  13884  issubg2m  13994  isnsg3  14012  eqgid  14031  kerf1ghm  14079  lmodprop2d  14687  lsspropdg  14770  znidomb  14995  znrrg  14997  comet  15602  fsumcncntop  15670  mulcncf  15711  birthdaylem3  16095  mpodvdsmulf1o  16110  gausslemma2dlem0d  16183  gausslemma2dlem1a  16189  2lgslem1a1  16217  2sqlem8a  16253  2sqlem8  16254  trilpo  17104  neapmkv  17130