Theorem syl21anc 1198

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 305	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))
5		syl21anc.4	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
6	4, 5	syl 14	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107

This theorem is referenced by:  issod  4201  brcogw  4668  funprg  5131  funtpg  5132  fnunsn  5188  ftpg  5558  fsnunf  5574  isotr  5671  off  5948  caofrss  5960  tfr1onlembxssdm  6194  tfrcllembxssdm  6207  pmresg  6524  ac6sfi  6745  tridc  6746  fidcenumlemrks  6793  sbthlemi8  6804  casefun  6922  caseinj  6926  djufun  6941  djuinj  6943  mulclpi  7084  archnqq  7173  addlocprlemlt  7287  addlocprlemeq  7289  addlocprlemgt  7290  mullocprlem  7326  apreim  8283  ltrec1  8556  divge0d  9423  fseq1p1m1  9767  q2submod  10051  seq3caopr2  10148  seq3distr  10179  facavg  10385  shftfibg  10485  sqrtdiv  10706  sqrtdivd  10832  mulcn2  10973  demoivreALT  11330  dvdslegcd  11501  gcdnncl  11504  qredeu  11624  rpdvds  11626  rpexp  11677  oddpwdclemodd  11695  divnumden  11719  divdenle  11720  phimullem  11746  setsfun  11837  setsfun0  11838  strleund  11890  comet  12488  fsumcncntop  12542  mulcncf  12577  trilpo  12928