Theorem e11 45041

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

Syntax hints:   → wi 4  (   wvd1 44922

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 44923

This theorem is referenced by:  e11an  45042  e01  45044  e10  45047  elex2VD  45190  elex22VD  45191  eqsbc2VD  45192  tpid3gVD  45194  3ornot23VD  45199  orbi1rVD  45200  3orbi123VD  45202  sbc3orgVD  45203  ordelordALTVD  45219  sbcim2gVD  45227  trsbcVD  45229  undif3VD  45234  sbcssgVD  45235  csbingVD  45236  onfrALTVD  45243  csbeq2gVD  45244  csbsngVD  45245  csbxpgVD  45246  csbresgVD  45247  csbrngVD  45248  csbima12gALTVD  45249  csbunigVD  45250  csbfv12gALTVD  45251  19.41rgVD  45254  2pm13.193VD  45255  hbimpgVD  45256  ax6e2eqVD  45259  2uasbanhVD  45263  notnotrALTVD  45267