Theorem e1a 45812

Description: A Virtual deduction elimination rule. syl 18 is e1a 45812 without virtual deductions. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
e1a.1	⊢ (   𝜑   ▶   𝜓   )
e1a.2	⊢ (𝜓 → 𝜒)

Assertion

Ref	Expression
e1a	⊢ (   𝜑   ▶   𝜒   )

Proof of Theorem e1a

Step	Hyp	Ref	Expression
1		e1a.1	. . . 4 ⊢ (   𝜑   ▶   𝜓   )
2	1	in1 45756	. . 3 ⊢ (𝜑 → 𝜓)
3		e1a.2	. . 3 ⊢ (𝜓 → 𝜒)
4	2, 3	syl 18	. 2 ⊢ (𝜑 → 𝜒)
5	4	dfvd1ir 45758	1 ⊢ (   𝜑   ▶   𝜒   )

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

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 45755

This theorem is used by:  e1bi  45814  e1bir  45815  snelpwrVD  46015  unipwrVD  46016  sstrALT2VD  46018  elex2VD  46022  elex22VD  46023  eqsbc2VD  46024  zfregs2VD  46025  tpid3gVD  46026  en3lplem1VD  46027  en3lpVD  46029  3ornot23VD  46031  3orbi123VD  46034  sbc3orgVD  46035  exbirVD  46037  3impexpVD  46040  3impexpbicomVD  46041  tratrbVD  46045  al2imVD  46046  syl5impVD  46047  ssralv2VD  46050  ordelordALTVD  46051  sbcim2gVD  46059  trsbcVD  46061  truniALTVD  46062  trintALTVD  46064  undif3VD  46066  sbcssgVD  46067  csbingVD  46068  onfrALTlem3VD  46071  simplbi2comtVD  46072  onfrALTlem2VD  46073  onfrALTVD  46075  csbeq2gVD  46076  csbsngVD  46077  csbxpgVD  46078  csbresgVD  46079  csbrngVD  46080  csbima12gALTVD  46081  csbunigVD  46082  csbfv12gALTVD  46083  con5VD  46084  relopabVD  46085  19.41rgVD  46086  2pm13.193VD  46087  hbimpgVD  46088  hbalgVD  46089  hbexgVD  46090  ax6e2eqVD  46091  ax6e2ndVD  46092  ax6e2ndeqVD  46093  2sb5ndVD  46094  2uasbanhVD  46095  e2ebindVD  46096  sb5ALTVD  46097  vk15.4jVD  46098  notnotrALTVD  46099  con3ALTVD  46100