Theorem ee222 44473

Description: e222 44607 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 406	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3		ee222.2	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜃))
4	3	imp 406	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5		ee222.3	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜏))
6	5	imp 406	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜏)
7		ee222.4	. . 3 ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))
8	2, 4, 6, 7	syl3c 66	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜂)
9	8	ex 412	1 ⊢ (𝜑 → (𝜓 → 𝜂))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ee121  44476  ee122  44477  tratrb  44507  ee220  44609  ee202  44611  ee022  44613  ee002  44615  ee020  44617  ee200  44619  ee221  44621  ee212  44623  ee112  44626  ee211  44629  ee210  44631  ee201  44633  ee120  44635  ee021  44637  ee012  44639  ee102  44641  suctrALT2  44808