Theorem syl21anc 1272

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  4416  brcogw  4899  funprg  5380  funtpg  5381  fnunsn  5439  fun2d  5510  ftpg  5838  fsnunf  5854  isotr  5957  off  6248  caofrss  6267  tfr1onlembxssdm  6509  tfrcllembxssdm  6522  pmresg  6845  ac6sfi  7087  tridc  7089  eqsndc  7095  tpfidceq  7122  fidcenumlemrks  7152  sbthlemi8  7163  casefun  7284  caseinj  7288  djufun  7303  djuinj  7305  mulclpi  7548  archnqq  7637  addlocprlemlt  7751  addlocprlemeq  7753  addlocprlemgt  7754  mullocprlem  7790  apreim  8783  subrecap  9019  ltrec1  9068  divge0d  9972  fseq1p1m1  10329  q2submod  10648  seq3caopr2  10756  seqcaopr2g  10757  seq3distr  10795  facavg  11009  swrdwrdsymbg  11249  cats1un  11306  shftfibg  11385  sqrtdiv  11607  sqrtdivd  11733  mulcn2  11877  demoivreALT  12340  dvdslegcd  12540  gcdnncl  12543  qredeu  12674  rpdvds  12676  rpexp  12730  oddpwdclemodd  12749  divnumden  12773  divdenle  12774  phimullem  12802  phisum  12818  pythagtriplem4  12846  pythagtriplem8  12850  pythagtriplem9  12851  pcgcd1  12906  fldivp1  12926  pockthlem  12934  setsfun  13122  setsfun0  13123  strleund  13191  ercpbl  13419  sgrppropd  13501  mndpropd  13528  grpidssd  13664  grpinvssd  13665  issubg2m  13781  isnsg3  13799  eqgid  13818  kerf1ghm  13866  lmodprop2d  14368  lsspropdg  14451  znidomb  14678  znrrg  14680  comet  15229  fsumcncntop  15297  mulcncf  15338  mpodvdsmulf1o  15720  gausslemma2dlem0d  15787  gausslemma2dlem1a  15793  2lgslem1a1  15821  2sqlem8a  15857  2sqlem8  15858  trilpo  16673  neapmkv  16698