Theorem syl21anc 1249

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  4371  brcogw  4852  funprg  5330  funtpg  5331  fnunsn  5389  fun2d  5458  ftpg  5778  fsnunf  5794  isotr  5895  off  6181  caofrss  6200  tfr1onlembxssdm  6439  tfrcllembxssdm  6452  pmresg  6773  ac6sfi  7007  tridc  7008  tpfidceq  7039  fidcenumlemrks  7067  sbthlemi8  7078  casefun  7199  caseinj  7203  djufun  7218  djuinj  7220  mulclpi  7454  archnqq  7543  addlocprlemlt  7657  addlocprlemeq  7659  addlocprlemgt  7660  mullocprlem  7696  apreim  8689  subrecap  8925  ltrec1  8974  divge0d  9872  fseq1p1m1  10229  q2submod  10543  seq3caopr2  10651  seqcaopr2g  10652  seq3distr  10690  facavg  10904  swrdwrdsymbg  11131  shftfibg  11181  sqrtdiv  11403  sqrtdivd  11529  mulcn2  11673  demoivreALT  12135  dvdslegcd  12335  gcdnncl  12338  qredeu  12469  rpdvds  12471  rpexp  12525  oddpwdclemodd  12544  divnumden  12568  divdenle  12569  phimullem  12597  phisum  12613  pythagtriplem4  12641  pythagtriplem8  12645  pythagtriplem9  12646  pcgcd1  12701  fldivp1  12721  pockthlem  12729  setsfun  12917  setsfun0  12918  strleund  12985  ercpbl  13213  sgrppropd  13295  mndpropd  13322  grpidssd  13458  grpinvssd  13459  issubg2m  13575  isnsg3  13593  eqgid  13612  kerf1ghm  13660  lmodprop2d  14160  lsspropdg  14243  znidomb  14470  znrrg  14472  comet  15021  fsumcncntop  15089  mulcncf  15130  mpodvdsmulf1o  15512  gausslemma2dlem0d  15579  gausslemma2dlem1a  15585  2lgslem1a1  15613  2sqlem8a  15649  2sqlem8  15650  trilpo  16097  neapmkv  16122