Theorem syl22anc 1183

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

Hypotheses

Ref	Expression
sylXanc.1	⊢ (φ → ψ)
sylXanc.2	⊢ (φ → χ)
sylXanc.3	⊢ (φ → θ)
sylXanc.4	⊢ (φ → τ)
syl22anc.5	⊢ (((ψ ∧ χ) ∧ (θ ∧ τ)) → η)

Assertion

Ref	Expression
syl22anc	⊢ (φ → η)

Proof of Theorem syl22anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 ⊢ (φ → ψ)
2		sylXanc.2	. . 3 ⊢ (φ → χ)
3	1, 2	jca 518	. 2 ⊢ (φ → (ψ ∧ χ))
4		sylXanc.3	. 2 ⊢ (φ → θ)
5		sylXanc.4	. 2 ⊢ (φ → τ)
6		syl22anc.5	. 2 ⊢ (((ψ ∧ χ) ∧ (θ ∧ τ)) → η)
7	3, 4, 5, 6	syl12anc 1180	1 ⊢ (φ → η)

Syntax hints:   → wi 4   ∧ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  prepeano4  4451  preaddccan2  4455  ncfindi  4475  ncfinsn  4476  ncfineleq  4477  nnpw1ex  4484  tfin11  4493  tfinpw1  4494  ncfintfin  4495  tfindi  4496  tfinsuc  4498  evenodddisj  4516  sfin112  4529  vfintle  4546  vfinspsslem1  4550  vfinncsp  4554  enadj  6060  ncdisjun  6136  nntccl  6170  ceclnn1  6189  sbth  6206  tcncg  6224  cet  6234  spacis  6288  nchoicelem6  6294