Theorem syl21anc 1277

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  4462  brcogw  4947  funprg  5429  funtpg  5430  fnunsn  5488  fun2d  5561  ftpg  5893  fsnunf  5909  isotr  6016  off  6309  caofrss  6328  suppssfvg  6497  tfr1onlembxssdm  6608  tfrcllembxssdm  6621  pmresg  6951  ac6sfi  7196  tridc  7198  eqsndc  7204  tpfidceq  7231  fidcenumlemrks  7264  sbthlemi8  7275  casefun  7419  caseinj  7423  djufun  7438  djuinj  7440  mulclpi  7689  archnqq  7778  addlocprlemlt  7892  addlocprlemeq  7894  addlocprlemgt  7895  mullocprlem  7931  apreim  8925  subrecap  9163  ltrec1  9212  divge0d  10121  fseq1p1m1  10484  q2submod  10805  seq3caopr2  10913  seqcaopr2g  10914  seq3distr  10952  facavg  11167  swrdwrdsymbg  11419  cats1un  11476  shftfibg  11568  sqrtdiv  11791  sqrtdivd  11917  mulcn2  12061  demoivreALT  12524  dvdslegcd  12724  gcdnncl  12727  qredeu  12858  rpdvds  12860  rpexp  12914  oddpwdclemodd  12933  divnumden  12957  divdenle  12958  phimullem  12986  phisum  13002  pythagtriplem4  13030  pythagtriplem8  13034  pythagtriplem9  13035  pcgcd1  13090  fldivp1  13110  pockthlem  13118  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemfrcn0  13256  setsfun  13370  setsfun0  13371  strleund  13440  ercpbl  13635  sgrppropd  13711  mndpropd  13736  grpidssd  13864  grpinvssd  13865  issubg2m  13975  isnsg3  13993  eqgid  14012  kerf1ghm  14060  lmodprop2d  14668  lsspropdg  14751  znidomb  14976  znrrg  14978  comet  15583  fsumcncntop  15651  mulcncf  15692  birthdaylem3  16072  mpodvdsmulf1o  16087  gausslemma2dlem0d  16154  gausslemma2dlem1a  16160  2lgslem1a1  16188  2sqlem8a  16224  2sqlem8  16225  trilpo  17066  neapmkv  17092