Theorem syl21anc 1270

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  4414  brcogw  4897  funprg  5377  funtpg  5378  fnunsn  5436  fun2d  5507  ftpg  5833  fsnunf  5849  isotr  5952  off  6243  caofrss  6262  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  pmresg  6840  ac6sfi  7082  tridc  7084  eqsndc  7090  tpfidceq  7117  fidcenumlemrks  7146  sbthlemi8  7157  casefun  7278  caseinj  7282  djufun  7297  djuinj  7299  mulclpi  7541  archnqq  7630  addlocprlemlt  7744  addlocprlemeq  7746  addlocprlemgt  7747  mullocprlem  7783  apreim  8776  subrecap  9012  ltrec1  9061  divge0d  9965  fseq1p1m1  10322  q2submod  10640  seq3caopr2  10748  seqcaopr2g  10749  seq3distr  10787  facavg  11001  swrdwrdsymbg  11238  cats1un  11295  shftfibg  11374  sqrtdiv  11596  sqrtdivd  11722  mulcn2  11866  demoivreALT  12328  dvdslegcd  12528  gcdnncl  12531  qredeu  12662  rpdvds  12664  rpexp  12718  oddpwdclemodd  12737  divnumden  12761  divdenle  12762  phimullem  12790  phisum  12806  pythagtriplem4  12834  pythagtriplem8  12838  pythagtriplem9  12839  pcgcd1  12894  fldivp1  12914  pockthlem  12922  setsfun  13110  setsfun0  13111  strleund  13179  ercpbl  13407  sgrppropd  13489  mndpropd  13516  grpidssd  13652  grpinvssd  13653  issubg2m  13769  isnsg3  13787  eqgid  13806  kerf1ghm  13854  lmodprop2d  14355  lsspropdg  14438  znidomb  14665  znrrg  14667  comet  15216  fsumcncntop  15284  mulcncf  15325  mpodvdsmulf1o  15707  gausslemma2dlem0d  15774  gausslemma2dlem1a  15780  2lgslem1a1  15808  2sqlem8a  15844  2sqlem8  15845  trilpo  16597  neapmkv  16622