Theorem e11 45438

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

This proof depends on syntax axioms:   → wi 4  (   wvd1 45319

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-vd1 45320

This theorem is used by:  e11an  45439  e01  45441  e10  45444  elex2VD  45587  elex22VD  45588  eqsbc2VD  45589  tpid3gVD  45591  3ornot23VD  45596  orbi1rVD  45597  3orbi123VD  45599  sbc3orgVD  45600  ordelordALTVD  45616  sbcim2gVD  45624  trsbcVD  45626  undif3VD  45631  sbcssgVD  45632  csbingVD  45633  onfrALTVD  45640  csbeq2gVD  45641  csbsngVD  45642  csbxpgVD  45643  csbresgVD  45644  csbrngVD  45645  csbima12gALTVD  45646  csbunigVD  45647  csbfv12gALTVD  45648  19.41rgVD  45651  2pm13.193VD  45652  hbimpgVD  45653  ax6e2eqVD  45656  2uasbanhVD  45660  notnotrALTVD  45664