Theorem e11 45764

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

Hypotheses

Ref	Expression
e11.1	⊢ (   𝜑   ▶   𝜓   )
e11.2	⊢ (   𝜑   ▶   𝜒   )
e11.3	⊢ (𝜓 → (𝜒 → 𝜃))

Assertion

Ref	Expression
e11	⊢ (   𝜑   ▶   𝜃   )

Proof of Theorem e11

Step	Hyp	Ref	Expression
1		e11.1	. 2 ⊢ (   𝜑   ▶   𝜓   )
2		e11.2	. 2 ⊢ (   𝜑   ▶   𝜒   )
3		e11.3	. . 3 ⊢ (𝜓 → (𝜒 → 𝜃))
4	3	a1i 11	. 2 ⊢ (𝜓 → (𝜓 → (𝜒 → 𝜃)))
5	1, 1, 2, 4	e111 45750	1 ⊢ (   𝜑   ▶   𝜃   )

This proof depends on syntax axioms:   → wi 4  (   wvd1 45645

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-vd1 45646

This theorem is used by:  e11an  45765  e01  45767  e10  45770  elex2VD  45913  elex22VD  45914  eqsbc2VD  45915  tpid3gVD  45917  3ornot23VD  45922  orbi1rVD  45923  3orbi123VD  45925  sbc3orgVD  45926  ordelordALTVD  45942  sbcim2gVD  45950  trsbcVD  45952  undif3VD  45957  sbcssgVD  45958  csbingVD  45959  onfrALTVD  45966  csbeq2gVD  45967  csbsngVD  45968  csbxpgVD  45969  csbresgVD  45970  csbrngVD  45971  csbima12gALTVD  45972  csbunigVD  45973  csbfv12gALTVD  45974  19.41rgVD  45977  2pm13.193VD  45978  hbimpgVD  45979  ax6e2eqVD  45982  2uasbanhVD  45986  notnotrALTVD  45990