Theorem e22 39719

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 39684	1 ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )

Syntax hints:   → wi 4  (   wvd2 39616

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 199  df-an 387  df-vd2 39617

This theorem is referenced by:  e22an  39720  e02  39745  e12  39773  e20  39776  e21  39779  sspwtr  39870  pwtrVD  39873  pwtrrVD  39874  elex22VD  39888  tpid3gVD  39891  en3lplem2VD  39893  imbi12VD  39922  truniALTVD  39927  trintALTVD  39929  onfrALTlem3VD  39936  onfrALTlem2VD  39938  ax6e2eqVD  39956  ax6e2ndeqVD  39958  sb5ALTVD  39962