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  4422  brcogw  4905  funprg  5387  funtpg  5388  fnunsn  5446  fun2d  5518  ftpg  5846  fsnunf  5862  isotr  5967  off  6257  caofrss  6276  suppssfvg  6441  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  pmresg  6888  ac6sfi  7130  tridc  7132  eqsndc  7138  tpfidceq  7165  fidcenumlemrks  7195  sbthlemi8  7206  casefun  7327  caseinj  7331  djufun  7346  djuinj  7348  mulclpi  7591  archnqq  7680  addlocprlemlt  7794  addlocprlemeq  7796  addlocprlemgt  7797  mullocprlem  7833  apreim  8826  subrecap  9062  ltrec1  9111  divge0d  10015  fseq1p1m1  10372  q2submod  10691  seq3caopr2  10799  seqcaopr2g  10800  seq3distr  10838  facavg  11052  swrdwrdsymbg  11292  cats1un  11349  shftfibg  11441  sqrtdiv  11663  sqrtdivd  11789  mulcn2  11933  demoivreALT  12396  dvdslegcd  12596  gcdnncl  12599  qredeu  12730  rpdvds  12732  rpexp  12786  oddpwdclemodd  12805  divnumden  12829  divdenle  12830  phimullem  12858  phisum  12874  pythagtriplem4  12902  pythagtriplem8  12906  pythagtriplem9  12907  pcgcd1  12962  fldivp1  12982  pockthlem  12990  setsfun  13178  setsfun0  13179  strleund  13247  ercpbl  13475  sgrppropd  13557  mndpropd  13584  grpidssd  13720  grpinvssd  13721  issubg2m  13837  isnsg3  13855  eqgid  13874  kerf1ghm  13922  lmodprop2d  14424  lsspropdg  14507  znidomb  14734  znrrg  14736  comet  15290  fsumcncntop  15358  mulcncf  15399  mpodvdsmulf1o  15784  gausslemma2dlem0d  15851  gausslemma2dlem1a  15857  2lgslem1a1  15885  2sqlem8a  15921  2sqlem8  15922  trilpo  16755  neapmkv  16781