Theorem syl21anc 1273

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  4439  brcogw  4923  funprg  5405  funtpg  5406  fnunsn  5464  fun2d  5537  ftpg  5867  fsnunf  5883  isotr  5988  off  6278  caofrss  6297  suppssfvg  6462  tfr1onlembxssdm  6573  tfrcllembxssdm  6586  pmresg  6909  ac6sfi  7154  tridc  7156  eqsndc  7162  tpfidceq  7189  fidcenumlemrks  7222  sbthlemi8  7233  casefun  7375  caseinj  7379  djufun  7394  djuinj  7396  mulclpi  7642  archnqq  7731  addlocprlemlt  7845  addlocprlemeq  7847  addlocprlemgt  7848  mullocprlem  7884  apreim  8876  subrecap  9112  ltrec1  9161  divge0d  10069  fseq1p1m1  10427  q2submod  10746  seq3caopr2  10854  seqcaopr2g  10855  seq3distr  10893  facavg  11107  swrdwrdsymbg  11352  cats1un  11409  shftfibg  11501  sqrtdiv  11723  sqrtdivd  11849  mulcn2  11993  demoivreALT  12456  dvdslegcd  12656  gcdnncl  12659  qredeu  12790  rpdvds  12792  rpexp  12846  oddpwdclemodd  12865  divnumden  12889  divdenle  12890  phimullem  12918  phisum  12934  pythagtriplem4  12962  pythagtriplem8  12966  pythagtriplem9  12967  pcgcd1  13022  fldivp1  13042  pockthlem  13050  setsfun  13239  setsfun0  13240  strleund  13308  ercpbl  13536  sgrppropd  13618  mndpropd  13645  grpidssd  13781  grpinvssd  13782  issubg2m  13898  isnsg3  13916  eqgid  13935  kerf1ghm  13983  lmodprop2d  14488  lsspropdg  14571  znidomb  14798  znrrg  14800  comet  15356  fsumcncntop  15424  mulcncf  15465  mpodvdsmulf1o  15850  gausslemma2dlem0d  15917  gausslemma2dlem1a  15923  2lgslem1a1  15951  2sqlem8a  15987  2sqlem8  15988  trilpo  16819  neapmkv  16845