Theorem e11 37934

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

Syntax hints:   → wi 4  (   wvd1 37806

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 196  df-vd1 37807

This theorem is referenced by:  e11an  37935  e01  37937  e10  37940  elex2VD  38095  elex22VD  38096  eqsbc3rVD  38097  tpid3gVD  38099  3ornot23VD  38104  orbi1rVD  38105  3orbi123VD  38107  sbc3orgVD  38108  sbcoreleleqVD  38117  ordelordALTVD  38125  sbcim2gVD  38133  trsbcVD  38135  undif3VD  38140  sbcssgVD  38141  csbingVD  38142  onfrALTVD  38149  csbeq2gVD  38150  csbsngVD  38151  csbxpgVD  38152  csbresgVD  38153  csbrngVD  38154  csbima12gALTVD  38155  csbunigVD  38156  csbfv12gALTVD  38157  19.41rgVD  38160  2pm13.193VD  38161  hbimpgVD  38162  ax6e2eqVD  38165  2uasbanhVD  38169  notnotrALTVD  38173