Theorem syl122anc 1283

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 1279	1 ⊢ (𝜑 → 𝜁)

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

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 1007

This theorem is referenced by:  divdiv32apd  9110  divcanap5d  9111  divcanap7d  9113  divdivap1d  9116  divdivap2d  9117  seq3coll  11242  cau3lem  11828  summodclem2a  12096  prodmodclem2a  12291  prmind2  12846  divnumden  12922  pceulem  13021  pcqmul  13030  pcqdiv  13034  pcexp  13036  pcaddlem  13066  pcbc  13078  abladdsub4  14071  ablpnpcan  14077  lmodvs1  14594  blss2ps  15401  blss2  15402  blssps  15422  blss  15423  xmeter  15431  lgsdi  16040