Theorem ee222 45485

Description: e222 45619 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 7-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
ee222.1	⊢ (𝜑 → (𝜓 → 𝜒))
ee222.2	⊢ (𝜑 → (𝜓 → 𝜃))
ee222.3	⊢ (𝜑 → (𝜓 → 𝜏))
ee222.4	⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))

Assertion

Ref	Expression
ee222	⊢ (𝜑 → (𝜓 → 𝜂))

Proof of Theorem ee222

Step	Hyp	Ref	Expression
1		ee222.1	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	imp 412	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3		ee222.2	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜃))
4	3	imp 412	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5		ee222.3	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜏))
6	5	imp 412	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜏)
7		ee222.4	. . 3 ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))
8	2, 4, 6, 7	syl3c 67	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜂)
9	8	ex 418	1 ⊢ (𝜑 → (𝜓 → 𝜂))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ee121  45488  ee122  45489  tratrb  45519  ee220  45621  ee202  45623  ee022  45625  ee002  45627  ee020  45629  ee200  45631  ee221  45633  ee212  45635  ee112  45638  ee211  45641  ee210  45643  ee201  45645  ee120  45647  ee021  45649  ee012  45651  ee102  45653  suctrALT2  45819