Theorem ee222 45674

Description: e222 45808 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  45677  ee122  45678  tratrb  45708  ee220  45810  ee202  45812  ee022  45814  ee002  45816  ee020  45818  ee200  45820  ee221  45822  ee212  45824  ee112  45827  ee211  45830  ee210  45832  ee201  45834  ee120  45836  ee021  45838  ee012  45840  ee102  45842  suctrALT2  46008