Theorem syl13anc 1219

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
sylXanc.1	⊢ (𝜑 → 𝜓)
sylXanc.2	⊢ (𝜑 → 𝜒)
sylXanc.3	⊢ (𝜑 → 𝜃)
sylXanc.4	⊢ (𝜑 → 𝜏)
syl13anc.5	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂)

Assertion

Ref	Expression
syl13anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl13anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. 2 ⊢ (𝜑 → 𝜓)
2		sylXanc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		sylXanc.3	. . 3 ⊢ (𝜑 → 𝜃)
4		sylXanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5	2, 3, 4	3jca 1162	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
6		syl13anc.5	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂)
7	1, 5, 6	syl2anc 409	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 963

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

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  syl23anc  1224  syl33anc  1232  caovassd  5938  caovcand  5941  caovordid  5945  caovordd  5947  caovdid  5954  caovdird  5957  swoer  6465  swoord1  6466  swoord2  6467  fimax2gtrilemstep  6802  iunfidisj  6842  ssfii  6870  suplub2ti  6896  prarloclem3  7329  fzosubel3  10004  seq3split  10283  seq3caopr  10287  zsumdc  11185  fsumiun  11278  divalglemex  11655  strle1g  12088  psmetsym  12537  psmettri  12538  psmetge0  12539  psmetres2  12541  xmetge0  12573  xmetsym  12576  xmettri  12580  metrtri  12585  xmetres2  12587  bldisj  12609  xblss2ps  12612  xblss2  12613  xmeter  12644  xmetxp  12715