Theorem ee222 44887

Description: e222 45021 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  44890  ee122  44891  tratrb  44921  ee220  45023  ee202  45025  ee022  45027  ee002  45029  ee020  45031  ee200  45033  ee221  45035  ee212  45037  ee112  45040  ee211  45043  ee210  45045  ee201  45047  ee120  45049  ee021  45051  ee012  45053  ee102  45055  suctrALT2  45221