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  6619  tfrcllembxssdm  6632  pmresg  6962  ac6sfi  7208  tridc  7210  eqsndc  7216  tpfidceq  7243  fidcenumlemrks  7277  sbthlemi8  7288  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  10155  fseq1p1m1  10518  q2submod  10843  seq3caopr2  10951  seqcaopr2g  10952  seq3distr  10990  facavg  11206  swrdwrdsymbg  11458  cats1un  11515  shftfibg  11607  sqrtdiv  11830  sqrtdivd  11957  mulcn2  12103  demoivreALT  12566  dvdslegcd  12766  gcdnncl  12769  qredeu  12900  rpdvds  12902  rpexp  12957  nnmaxpwlemnfac  12976  nnmaxpwlemparts  12977  divnumden  13001  divdenle  13002  phimullem  13032  phisum  13048  pythagtriplem4  13076  pythagtriplem8  13080  pythagtriplem9  13081  pcgcd1  13136  fldivp1  13156  pockthlem  13164  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemfrcn0  13331  setsfun  13445  setsfun0  13446  strleund  13516  ercpbl  13711  sgrppropd  13787  mndpropd  13812  grpidssd  13940  grpinvssd  13941  issubg2m  14051  isnsg3  14069  eqgid  14088  kerf1ghm  14136  lmodprop2d  14794  lsspropdg  14877  znidomb  15102  znrrg  15104  comet  15758  fsumcncntop  15826  mulcncf  15867  zprmlogbaplem2  16249  birthdaylem3  16260  mpodvdsmulf1o  16317  gausslemma2dlem0d  16409  gausslemma2dlem1a  16415  2lgslem1a1  16443  2sqlem8a  16479  2sqlem8  16480  trilpo  17332  neapmkv  17358