Theorem e22 45856

Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
e22.1	⊢ (   𝜑   ,   𝜓   ▶   𝜒   )
e22.2	⊢ (   𝜑   ,   𝜓   ▶   𝜃   )
e22.3	⊢ (𝜒 → (𝜃 → 𝜏))

Assertion

Ref	Expression
e22	⊢ (   𝜑   ,   𝜓   ▶   𝜏   )

Proof of Theorem e22

Step	Hyp	Ref	Expression
1		e22.1	. 2 ⊢ (   𝜑   ,   𝜓   ▶   𝜒   )
2		e22.2	. 2 ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )
3		e22.3	. . 3 ⊢ (𝜒 → (𝜃 → 𝜏))
4	3	a1i 11	. 2 ⊢ (𝜒 → (𝜒 → (𝜃 → 𝜏)))
5	1, 1, 2, 4	e222 45821	1 ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )

This proof depends on syntax axioms:   → wi 4  (   wvd2 45762

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  df-vd2 45763

This theorem is used by:  e22an  45857  e02  45882  e12  45908  e20  45911  e21  45914  sspwtr  46005  pwtrVD  46008  pwtrrVD  46009  elex22VD  46023  tpid3gVD  46026  en3lplem2VD  46028  imbi12VD  46057  truniALTVD  46062  trintALTVD  46064  onfrALTlem3VD  46071  onfrALTlem2VD  46073  ax6e2eqVD  46091  ax6e2ndeqVD  46093  sb5ALTVD  46097