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  5970  caovcand  5973  caovordid  5977  caovordd  5979  caovdid  5986  caovdird  5989  swoer  6497  swoord1  6498  swoord2  6499  fimax2gtrilemstep  6834  iunfidisj  6879  ssfii  6907  suplub2ti  6933  prarloclem3  7396  fzosubel3  10073  seq3split  10356  seq3caopr  10360  zsumdc  11258  fsumiun  11351  divalglemex  11786  strle1g  12219  psmetsym  12668  psmettri  12669  psmetge0  12670  psmetres2  12672  xmetge0  12704  xmetsym  12707  xmettri  12711  metrtri  12716  xmetres2  12718  bldisj  12740  xblss2ps  12743  xblss2  12744  xmeter  12775  xmetxp  12846