Theorem syl21anc 1168

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  issod  4074  brcogw  4522  funprg  4969  funtpg  4970  fnunsn  5026  ftpg  5368  fsnunf  5383  isotr  5476  off  5744  caofrss  5755  ac6sfi  6379  mulclpi  6518  archnqq  6607  addlocprlemlt  6721  addlocprlemeq  6723  addlocprlemgt  6724  mullocprlem  6760  apreim  7703  ltrec1  7966  divge0d  8814  fseq1p1m1  9111  q2submod  9387  iseqcaopr2  9461  iseqdistr  9470  facavg  9673  shftfibg  9708  sqrtdiv  9928  sqrtdivd  10054  mulcn2  10151  dvdslegcd  10356  gcdnncl  10359  qredeu  10479  rpdvds  10481  rpexp  10532  oddpwdclemodd  10550