Theorem ee222 45239

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

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

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 401

This theorem is used by:  ee121  45242  ee122  45243  tratrb  45273  ee220  45375  ee202  45377  ee022  45379  ee002  45381  ee020  45383  ee200  45385  ee221  45387  ee212  45389  ee112  45392  ee211  45395  ee210  45397  ee201  45399  ee120  45401  ee021  45403  ee012  45405  ee102  45407  suctrALT2  45573