Theorem syl21anc 1248

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  4355  brcogw  4836  funprg  5309  funtpg  5310  fnunsn  5368  ftpg  5749  fsnunf  5765  isotr  5866  off  6152  caofrss  6171  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  pmresg  6744  ac6sfi  6968  tridc  6969  tpfidceq  7000  fidcenumlemrks  7028  sbthlemi8  7039  casefun  7160  caseinj  7164  djufun  7179  djuinj  7181  mulclpi  7414  archnqq  7503  addlocprlemlt  7617  addlocprlemeq  7619  addlocprlemgt  7620  mullocprlem  7656  apreim  8649  subrecap  8885  ltrec1  8934  divge0d  9831  fseq1p1m1  10188  q2submod  10496  seq3caopr2  10604  seqcaopr2g  10605  seq3distr  10643  facavg  10857  shftfibg  11004  sqrtdiv  11226  sqrtdivd  11352  mulcn2  11496  demoivreALT  11958  dvdslegcd  12158  gcdnncl  12161  qredeu  12292  rpdvds  12294  rpexp  12348  oddpwdclemodd  12367  divnumden  12391  divdenle  12392  phimullem  12420  phisum  12436  pythagtriplem4  12464  pythagtriplem8  12468  pythagtriplem9  12469  pcgcd1  12524  fldivp1  12544  pockthlem  12552  setsfun  12740  setsfun0  12741  strleund  12808  ercpbl  13035  sgrppropd  13117  mndpropd  13144  grpidssd  13280  grpinvssd  13281  issubg2m  13397  isnsg3  13415  eqgid  13434  kerf1ghm  13482  lmodprop2d  13982  lsspropdg  14065  znidomb  14292  znrrg  14294  comet  14843  fsumcncntop  14911  mulcncf  14952  mpodvdsmulf1o  15334  gausslemma2dlem0d  15401  gausslemma2dlem1a  15407  2lgslem1a1  15435  2sqlem8a  15471  2sqlem8  15472  trilpo  15800  neapmkv  15825