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  4411  brcogw  4894  funprg  5374  funtpg  5375  fnunsn  5433  fun2d  5504  ftpg  5830  fsnunf  5846  isotr  5949  off  6240  caofrss  6259  tfr1onlembxssdm  6500  tfrcllembxssdm  6513  pmresg  6836  ac6sfi  7073  tridc  7075  eqsndc  7081  tpfidceq  7108  fidcenumlemrks  7136  sbthlemi8  7147  casefun  7268  caseinj  7272  djufun  7287  djuinj  7289  mulclpi  7531  archnqq  7620  addlocprlemlt  7734  addlocprlemeq  7736  addlocprlemgt  7737  mullocprlem  7773  apreim  8766  subrecap  9002  ltrec1  9051  divge0d  9950  fseq1p1m1  10307  q2submod  10624  seq3caopr2  10732  seqcaopr2g  10733  seq3distr  10771  facavg  10985  swrdwrdsymbg  11217  cats1un  11274  shftfibg  11352  sqrtdiv  11574  sqrtdivd  11700  mulcn2  11844  demoivreALT  12306  dvdslegcd  12506  gcdnncl  12509  qredeu  12640  rpdvds  12642  rpexp  12696  oddpwdclemodd  12715  divnumden  12739  divdenle  12740  phimullem  12768  phisum  12784  pythagtriplem4  12812  pythagtriplem8  12816  pythagtriplem9  12817  pcgcd1  12872  fldivp1  12892  pockthlem  12900  setsfun  13088  setsfun0  13089  strleund  13157  ercpbl  13385  sgrppropd  13467  mndpropd  13494  grpidssd  13630  grpinvssd  13631  issubg2m  13747  isnsg3  13765  eqgid  13784  kerf1ghm  13832  lmodprop2d  14333  lsspropdg  14416  znidomb  14643  znrrg  14645  comet  15194  fsumcncntop  15262  mulcncf  15303  mpodvdsmulf1o  15685  gausslemma2dlem0d  15752  gausslemma2dlem1a  15758  2lgslem1a1  15786  2sqlem8a  15822  2sqlem8  15823  trilpo  16525  neapmkv  16550