Theorem e11 41028

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

Syntax hints:   → wi 4  (   wvd1 40909

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 40910

This theorem is referenced by:  e11an  41029  e01  41031  e10  41034  elex2VD  41178  elex22VD  41179  eqsbc3rVD  41180  tpid3gVD  41182  3ornot23VD  41187  orbi1rVD  41188  3orbi123VD  41190  sbc3orgVD  41191  ordelordALTVD  41207  sbcim2gVD  41215  trsbcVD  41217  undif3VD  41222  sbcssgVD  41223  csbingVD  41224  onfrALTVD  41231  csbeq2gVD  41232  csbsngVD  41233  csbxpgVD  41234  csbresgVD  41235  csbrngVD  41236  csbima12gALTVD  41237  csbunigVD  41238  csbfv12gALTVD  41239  19.41rgVD  41242  2pm13.193VD  41243  hbimpgVD  41244  ax6e2eqVD  41247  2uasbanhVD  41251  notnotrALTVD  41255