Theorem syl21anc 1273

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  4445  brcogw  4929  funprg  5411  funtpg  5412  fnunsn  5470  fun2d  5543  ftpg  5873  fsnunf  5889  isotr  5995  off  6288  caofrss  6307  suppssfvg  6476  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  pmresg  6923  ac6sfi  7168  tridc  7170  eqsndc  7176  tpfidceq  7203  fidcenumlemrks  7236  sbthlemi8  7247  casefun  7389  caseinj  7393  djufun  7408  djuinj  7410  mulclpi  7659  archnqq  7748  addlocprlemlt  7862  addlocprlemeq  7864  addlocprlemgt  7865  mullocprlem  7901  apreim  8894  subrecap  9130  ltrec1  9179  divge0d  10088  fseq1p1m1  10450  q2submod  10771  seq3caopr2  10879  seqcaopr2g  10880  seq3distr  10918  facavg  11133  swrdwrdsymbg  11381  cats1un  11438  shftfibg  11530  sqrtdiv  11752  sqrtdivd  11878  mulcn2  12022  demoivreALT  12485  dvdslegcd  12685  gcdnncl  12688  qredeu  12819  rpdvds  12821  rpexp  12875  oddpwdclemodd  12894  divnumden  12918  divdenle  12919  phimullem  12947  phisum  12963  pythagtriplem4  12991  pythagtriplem8  12995  pythagtriplem9  12996  pcgcd1  13051  fldivp1  13071  pockthlem  13079  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemfrcn0  13217  setsfun  13331  setsfun0  13332  strleund  13400  ercpbl  13628  sgrppropd  13710  mndpropd  13737  grpidssd  13873  grpinvssd  13874  issubg2m  13990  isnsg3  14008  eqgid  14027  kerf1ghm  14075  lmodprop2d  14608  lsspropdg  14691  znidomb  14918  znrrg  14920  comet  15476  fsumcncntop  15544  mulcncf  15585  mpodvdsmulf1o  15970  gausslemma2dlem0d  16037  gausslemma2dlem1a  16043  2lgslem1a1  16071  2sqlem8a  16107  2sqlem8  16108  trilpo  16939  neapmkv  16966