Theorem syl122anc 1280

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

Hypotheses

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

Assertion

Ref	Expression
syl122anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl122anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. 2 ⊢ (𝜑 → 𝜓)
2		sylXanc.2	. 2 ⊢ (𝜑 → 𝜒)
3		sylXanc.3	. 2 ⊢ (𝜑 → 𝜃)
4		sylXanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5		sylXanc.5	. . 3 ⊢ (𝜑 → 𝜂)
6	4, 5	jca 306	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl122anc.6	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 3, 6, 7	syl121anc 1276	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1002

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

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  divdiv32apd  8979  divcanap5d  8980  divcanap7d  8982  divdivap1d  8985  divdivap2d  8986  seq3coll  11082  cau3lem  11646  summodclem2a  11913  prodmodclem2a  12108  prmind2  12663  divnumden  12739  pceulem  12838  pcqmul  12847  pcqdiv  12851  pcexp  12853  pcaddlem  12883  pcbc  12895  abladdsub4  13872  ablpnpcan  13878  lmodvs1  14301  blss2ps  15101  blss2  15102  blssps  15122  blss  15123  xmeter  15131  lgsdi  15737