Theorem e1a 44340

Description: A Virtual deduction elimination rule. syl 17 is e1a 44340 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 44284	. . 3 ⊢ (𝜑 → 𝜓)
3		e1a.2	. . 3 ⊢ (𝜓 → 𝜒)
4	2, 3	syl 17	. 2 ⊢ (𝜑 → 𝜒)
5	4	dfvd1ir 44286	1 ⊢ (   𝜑   ▶   𝜒   )

Syntax hints:   → wi 4  (   wvd1 44282

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 206  df-vd1 44283

This theorem is referenced by:  e1bi  44342  e1bir  44343  snelpwrVD  44544  unipwrVD  44545  sstrALT2VD  44547  elex2VD  44551  elex22VD  44552  eqsbc2VD  44553  zfregs2VD  44554  tpid3gVD  44555  en3lplem1VD  44556  en3lpVD  44558  3ornot23VD  44560  3orbi123VD  44563  sbc3orgVD  44564  exbirVD  44566  3impexpVD  44569  3impexpbicomVD  44570  tratrbVD  44574  al2imVD  44575  syl5impVD  44576  ssralv2VD  44579  ordelordALTVD  44580  sbcim2gVD  44588  trsbcVD  44590  truniALTVD  44591  trintALTVD  44593  undif3VD  44595  sbcssgVD  44596  csbingVD  44597  onfrALTlem3VD  44600  simplbi2comtVD  44601  onfrALTlem2VD  44602  onfrALTVD  44604  csbeq2gVD  44605  csbsngVD  44606  csbxpgVD  44607  csbresgVD  44608  csbrngVD  44609  csbima12gALTVD  44610  csbunigVD  44611  csbfv12gALTVD  44612  con5VD  44613  relopabVD  44614  19.41rgVD  44615  2pm13.193VD  44616  hbimpgVD  44617  hbalgVD  44618  hbexgVD  44619  ax6e2eqVD  44620  ax6e2ndVD  44621  ax6e2ndeqVD  44622  2sb5ndVD  44623  2uasbanhVD  44624  e2ebindVD  44625  sb5ALTVD  44626  vk15.4jVD  44627  notnotrALTVD  44628  con3ALTVD  44629