Theorem syl21anc 1270

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 ⊢ (𝜑 → 𝜏)

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:  issod  4410  brcogw  4891  funprg  5371  funtpg  5372  fnunsn  5430  fun2d  5501  ftpg  5827  fsnunf  5843  isotr  5946  off  6237  caofrss  6256  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  pmresg  6831  ac6sfi  7068  tridc  7069  tpfidceq  7100  fidcenumlemrks  7128  sbthlemi8  7139  casefun  7260  caseinj  7264  djufun  7279  djuinj  7281  mulclpi  7523  archnqq  7612  addlocprlemlt  7726  addlocprlemeq  7728  addlocprlemgt  7729  mullocprlem  7765  apreim  8758  subrecap  8994  ltrec1  9043  divge0d  9941  fseq1p1m1  10298  q2submod  10615  seq3caopr2  10723  seqcaopr2g  10724  seq3distr  10762  facavg  10976  swrdwrdsymbg  11204  cats1un  11261  shftfibg  11339  sqrtdiv  11561  sqrtdivd  11687  mulcn2  11831  demoivreALT  12293  dvdslegcd  12493  gcdnncl  12496  qredeu  12627  rpdvds  12629  rpexp  12683  oddpwdclemodd  12702  divnumden  12726  divdenle  12727  phimullem  12755  phisum  12771  pythagtriplem4  12799  pythagtriplem8  12803  pythagtriplem9  12804  pcgcd1  12859  fldivp1  12879  pockthlem  12887  setsfun  13075  setsfun0  13076  strleund  13144  ercpbl  13372  sgrppropd  13454  mndpropd  13481  grpidssd  13617  grpinvssd  13618  issubg2m  13734  isnsg3  13752  eqgid  13771  kerf1ghm  13819  lmodprop2d  14320  lsspropdg  14403  znidomb  14630  znrrg  14632  comet  15181  fsumcncntop  15249  mulcncf  15290  mpodvdsmulf1o  15672  gausslemma2dlem0d  15739  gausslemma2dlem1a  15745  2lgslem1a1  15773  2sqlem8a  15809  2sqlem8  15810  trilpo  16441  neapmkv  16466