Theorem e11 45115

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

Syntax hints:   → wi 4  (   wvd1 44996

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 207  df-vd1 44997

This theorem is referenced by:  e11an  45116  e01  45118  e10  45121  elex2VD  45264  elex22VD  45265  eqsbc2VD  45266  tpid3gVD  45268  3ornot23VD  45273  orbi1rVD  45274  3orbi123VD  45276  sbc3orgVD  45277  ordelordALTVD  45293  sbcim2gVD  45301  trsbcVD  45303  undif3VD  45308  sbcssgVD  45309  csbingVD  45310  onfrALTVD  45317  csbeq2gVD  45318  csbsngVD  45319  csbxpgVD  45320  csbresgVD  45321  csbrngVD  45322  csbima12gALTVD  45323  csbunigVD  45324  csbfv12gALTVD  45325  19.41rgVD  45328  2pm13.193VD  45329  hbimpgVD  45330  ax6e2eqVD  45333  2uasbanhVD  45337  notnotrALTVD  45341