Theorem syl13anc 1218

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 1161	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
6		syl13anc.5	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂)
7	1, 5, 6	syl2anc 408	1 ⊢ (𝜑 → 𝜂)

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

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 964

This theorem is referenced by:  syl23anc  1223  syl33anc  1231  caovassd  5930  caovcand  5933  caovordid  5937  caovordd  5939  caovdid  5946  caovdird  5949  swoer  6457  swoord1  6458  swoord2  6459  fimax2gtrilemstep  6794  iunfidisj  6834  ssfii  6862  suplub2ti  6888  prarloclem3  7308  fzosubel3  9976  seq3split  10255  seq3caopr  10259  zsumdc  11156  fsumiun  11249  divalglemex  11622  strle1g  12052  psmetsym  12501  psmettri  12502  psmetge0  12503  psmetres2  12505  xmetge0  12537  xmetsym  12540  xmettri  12544  metrtri  12549  xmetres2  12551  bldisj  12573  xblss2ps  12576  xblss2  12577  xmeter  12608  xmetxp  12679