Theorem e11 45224

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 45210	1 ⊢ (   𝜑   ▶   𝜃   )

Syntax hints:   → wi 4  (   wvd1 45105

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 209  df-vd1 45106

This theorem is referenced by:  e11an  45225  e01  45227  e10  45230  elex2VD  45373  elex22VD  45374  eqsbc2VD  45375  tpid3gVD  45377  3ornot23VD  45382  orbi1rVD  45383  3orbi123VD  45385  sbc3orgVD  45386  ordelordALTVD  45402  sbcim2gVD  45410  trsbcVD  45412  undif3VD  45417  sbcssgVD  45418  csbingVD  45419  onfrALTVD  45426  csbeq2gVD  45427  csbsngVD  45428  csbxpgVD  45429  csbresgVD  45430  csbrngVD  45431  csbima12gALTVD  45432  csbunigVD  45433  csbfv12gALTVD  45434  19.41rgVD  45437  2pm13.193VD  45438  hbimpgVD  45439  ax6e2eqVD  45442  2uasbanhVD  45446  notnotrALTVD  45450