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  4466  brcogw  4951  funprg  5434  funtpg  5435  fnunsn  5493  fun2d  5566  ftpg  5902  fsnunf  5918  isotr  6025  off  6319  caofrss  6338  suppssfvg  6507  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  pmresg  6961  ac6sfi  7207  tridc  7209  eqsndc  7215  tpfidceq  7242  fidcenumlemrks  7276  sbthlemi8  7287  casefun  7432  caseinj  7436  djufun  7451  djuinj  7453  mulclpi  7702  archnqq  7791  addlocprlemlt  7905  addlocprlemeq  7907  addlocprlemgt  7908  mullocprlem  7944  apreim  8940  subrecap  9178  ltrec1  9227  divge0d  10156  fseq1p1m1  10519  q2submod  10844  seq3caopr2  10952  seqcaopr2g  10953  seq3distr  10991  facavg  11207  swrdwrdsymbg  11459  cats1un  11516  shftfibg  11608  sqrtdiv  11831  sqrtdivd  11958  mulcn2  12104  demoivreALT  12567  dvdslegcd  12767  gcdnncl  12770  qredeu  12901  rpdvds  12903  rpexp  12958  nnmaxpwlemnfac  12977  nnmaxpwlemparts  12978  divnumden  13002  divdenle  13003  phimullem  13033  phisum  13049  pythagtriplem4  13077  pythagtriplem8  13081  pythagtriplem9  13082  pcgcd1  13137  fldivp1  13157  pockthlem  13165  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemfrcn0  13332  setsfun  13446  setsfun0  13447  strleund  13517  ercpbl  13712  sgrppropd  13788  mndpropd  13813  grpidssd  13941  grpinvssd  13942  issubg2m  14052  isnsg3  14070  eqgid  14089  kerf1ghm  14137  lmodprop2d  14795  lsspropdg  14878  znidomb  15103  znrrg  15105  comet  15737  fsumcncntop  15805  mulcncf  15846  zprmlogbaplem2  16228  birthdaylem3  16239  mpodvdsmulf1o  16296  gausslemma2dlem0d  16388  gausslemma2dlem1a  16394  2lgslem1a1  16422  2sqlem8a  16458  2sqlem8  16459  trilpo  17311  neapmkv  17337