Theorem e1a 44747

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

Syntax hints:   → wi 4  (   wvd1 44689

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 207  df-vd1 44690

This theorem is referenced by:  e1bi  44749  e1bir  44750  snelpwrVD  44950  unipwrVD  44951  sstrALT2VD  44953  elex2VD  44957  elex22VD  44958  eqsbc2VD  44959  zfregs2VD  44960  tpid3gVD  44961  en3lplem1VD  44962  en3lpVD  44964  3ornot23VD  44966  3orbi123VD  44969  sbc3orgVD  44970  exbirVD  44972  3impexpVD  44975  3impexpbicomVD  44976  tratrbVD  44980  al2imVD  44981  syl5impVD  44982  ssralv2VD  44985  ordelordALTVD  44986  sbcim2gVD  44994  trsbcVD  44996  truniALTVD  44997  trintALTVD  44999  undif3VD  45001  sbcssgVD  45002  csbingVD  45003  onfrALTlem3VD  45006  simplbi2comtVD  45007  onfrALTlem2VD  45008  onfrALTVD  45010  csbeq2gVD  45011  csbsngVD  45012  csbxpgVD  45013  csbresgVD  45014  csbrngVD  45015  csbima12gALTVD  45016  csbunigVD  45017  csbfv12gALTVD  45018  con5VD  45019  relopabVD  45020  19.41rgVD  45021  2pm13.193VD  45022  hbimpgVD  45023  hbalgVD  45024  hbexgVD  45025  ax6e2eqVD  45026  ax6e2ndVD  45027  ax6e2ndeqVD  45028  2sb5ndVD  45029  2uasbanhVD  45030  e2ebindVD  45031  sb5ALTVD  45032  vk15.4jVD  45033  notnotrALTVD  45034  con3ALTVD  45035