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  8895  subrecap  9133  ltrec1  9182  divge0d  10091  fseq1p1m1  10453  q2submod  10774  seq3caopr2  10882  seqcaopr2g  10883  seq3distr  10921  facavg  11136  swrdwrdsymbg  11384  cats1un  11441  shftfibg  11533  sqrtdiv  11756  sqrtdivd  11882  mulcn2  12026  demoivreALT  12489  dvdslegcd  12689  gcdnncl  12692  qredeu  12823  rpdvds  12825  rpexp  12879  oddpwdclemodd  12898  divnumden  12922  divdenle  12923  phimullem  12951  phisum  12967  pythagtriplem4  12995  pythagtriplem8  12999  pythagtriplem9  13000  pcgcd1  13055  fldivp1  13075  pockthlem  13083  ballotfilemfc0  13180  ballotfilemfcc  13181  ballotfilemfrcn0  13221  setsfun  13335  setsfun0  13336  strleund  13404  ercpbl  13599  sgrppropd  13680  mndpropd  13705  grpidssd  13835  grpinvssd  13836  issubg2m  13946  isnsg3  13964  eqgid  13983  kerf1ghm  14031  lmodprop2d  14626  lsspropdg  14709  znidomb  14936  znrrg  14938  comet  15494  fsumcncntop  15562  mulcncf  15603  mpodvdsmulf1o  15988  gausslemma2dlem0d  16055  gausslemma2dlem1a  16061  2lgslem1a1  16089  2sqlem8a  16125  2sqlem8  16126  trilpo  16967  neapmkv  16993