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  4351  brcogw  4832  funprg  5305  funtpg  5306  fnunsn  5362  ftpg  5743  fsnunf  5759  isotr  5860  off  6145  caofrss  6159  tfr1onlembxssdm  6398  tfrcllembxssdm  6411  pmresg  6732  ac6sfi  6956  tridc  6957  fidcenumlemrks  7014  sbthlemi8  7025  casefun  7146  caseinj  7150  djufun  7165  djuinj  7167  mulclpi  7390  archnqq  7479  addlocprlemlt  7593  addlocprlemeq  7595  addlocprlemgt  7596  mullocprlem  7632  apreim  8624  subrecap  8860  ltrec1  8909  divge0d  9806  fseq1p1m1  10163  q2submod  10459  seq3caopr2  10567  seqcaopr2g  10568  seq3distr  10606  facavg  10820  shftfibg  10967  sqrtdiv  11189  sqrtdivd  11315  mulcn2  11458  demoivreALT  11920  dvdslegcd  12104  gcdnncl  12107  qredeu  12238  rpdvds  12240  rpexp  12294  oddpwdclemodd  12313  divnumden  12337  divdenle  12338  phimullem  12366  phisum  12381  pythagtriplem4  12409  pythagtriplem8  12413  pythagtriplem9  12414  pcgcd1  12469  fldivp1  12489  pockthlem  12497  setsfun  12656  setsfun0  12657  strleund  12724  ercpbl  12917  sgrppropd  12999  mndpropd  13024  grpidssd  13151  grpinvssd  13152  issubg2m  13262  isnsg3  13280  eqgid  13299  kerf1ghm  13347  lmodprop2d  13847  lsspropdg  13930  znidomb  14157  znrrg  14159  comet  14678  fsumcncntop  14746  mulcncf  14787  gausslemma2dlem0d  15209  gausslemma2dlem1a  15215  2lgslem1a1  15243  2sqlem8a  15279  2sqlem8  15280  trilpo  15603  neapmkv  15628