Theorem syl21anc 1248

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  4354  brcogw  4835  funprg  5308  funtpg  5309  fnunsn  5365  ftpg  5746  fsnunf  5762  isotr  5863  off  6148  caofrss  6162  tfr1onlembxssdm  6401  tfrcllembxssdm  6414  pmresg  6735  ac6sfi  6959  tridc  6960  tpfidceq  6991  fidcenumlemrks  7019  sbthlemi8  7030  casefun  7151  caseinj  7155  djufun  7170  djuinj  7172  mulclpi  7395  archnqq  7484  addlocprlemlt  7598  addlocprlemeq  7600  addlocprlemgt  7601  mullocprlem  7637  apreim  8630  subrecap  8866  ltrec1  8915  divge0d  9812  fseq1p1m1  10169  q2submod  10477  seq3caopr2  10585  seqcaopr2g  10586  seq3distr  10624  facavg  10838  shftfibg  10985  sqrtdiv  11207  sqrtdivd  11333  mulcn2  11477  demoivreALT  11939  dvdslegcd  12131  gcdnncl  12134  qredeu  12265  rpdvds  12267  rpexp  12321  oddpwdclemodd  12340  divnumden  12364  divdenle  12365  phimullem  12393  phisum  12409  pythagtriplem4  12437  pythagtriplem8  12441  pythagtriplem9  12442  pcgcd1  12497  fldivp1  12517  pockthlem  12525  setsfun  12713  setsfun0  12714  strleund  12781  ercpbl  12974  sgrppropd  13056  mndpropd  13081  grpidssd  13208  grpinvssd  13209  issubg2m  13319  isnsg3  13337  eqgid  13356  kerf1ghm  13404  lmodprop2d  13904  lsspropdg  13987  znidomb  14214  znrrg  14216  comet  14735  fsumcncntop  14803  mulcncf  14844  mpodvdsmulf1o  15226  gausslemma2dlem0d  15293  gausslemma2dlem1a  15299  2lgslem1a1  15327  2sqlem8a  15363  2sqlem8  15364  trilpo  15687  neapmkv  15712