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  4350  brcogw  4831  funprg  5304  funtpg  5305  fnunsn  5361  ftpg  5742  fsnunf  5758  isotr  5859  off  6143  caofrss  6157  tfr1onlembxssdm  6396  tfrcllembxssdm  6409  pmresg  6730  ac6sfi  6954  tridc  6955  fidcenumlemrks  7012  sbthlemi8  7023  casefun  7144  caseinj  7148  djufun  7163  djuinj  7165  mulclpi  7388  archnqq  7477  addlocprlemlt  7591  addlocprlemeq  7593  addlocprlemgt  7594  mullocprlem  7630  apreim  8622  subrecap  8858  ltrec1  8907  divge0d  9803  fseq1p1m1  10160  q2submod  10456  seq3caopr2  10564  seqcaopr2g  10565  seq3distr  10603  facavg  10817  shftfibg  10964  sqrtdiv  11186  sqrtdivd  11312  mulcn2  11455  demoivreALT  11917  dvdslegcd  12101  gcdnncl  12104  qredeu  12235  rpdvds  12237  rpexp  12291  oddpwdclemodd  12310  divnumden  12334  divdenle  12335  phimullem  12363  phisum  12378  pythagtriplem4  12406  pythagtriplem8  12410  pythagtriplem9  12411  pcgcd1  12466  fldivp1  12486  pockthlem  12494  setsfun  12653  setsfun0  12654  strleund  12721  ercpbl  12914  sgrppropd  12996  mndpropd  13021  grpidssd  13148  grpinvssd  13149  issubg2m  13259  isnsg3  13277  eqgid  13296  kerf1ghm  13344  lmodprop2d  13844  lsspropdg  13927  znidomb  14146  znrrg  14148  comet  14667  fsumcncntop  14724  mulcncf  14762  gausslemma2dlem0d  15168  gausslemma2dlem1a  15174  2sqlem8a  15209  2sqlem8  15210  trilpo  15533  neapmkv  15558