Theorem e1a 44980

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

Syntax hints:   → wi 4  (   wvd1 44922

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 44923

This theorem is referenced by:  e1bi  44982  e1bir  44983  snelpwrVD  45183  unipwrVD  45184  sstrALT2VD  45186  elex2VD  45190  elex22VD  45191  eqsbc2VD  45192  zfregs2VD  45193  tpid3gVD  45194  en3lplem1VD  45195  en3lpVD  45197  3ornot23VD  45199  3orbi123VD  45202  sbc3orgVD  45203  exbirVD  45205  3impexpVD  45208  3impexpbicomVD  45209  tratrbVD  45213  al2imVD  45214  syl5impVD  45215  ssralv2VD  45218  ordelordALTVD  45219  sbcim2gVD  45227  trsbcVD  45229  truniALTVD  45230  trintALTVD  45232  undif3VD  45234  sbcssgVD  45235  csbingVD  45236  onfrALTlem3VD  45239  simplbi2comtVD  45240  onfrALTlem2VD  45241  onfrALTVD  45243  csbeq2gVD  45244  csbsngVD  45245  csbxpgVD  45246  csbresgVD  45247  csbrngVD  45248  csbima12gALTVD  45249  csbunigVD  45250  csbfv12gALTVD  45251  con5VD  45252  relopabVD  45253  19.41rgVD  45254  2pm13.193VD  45255  hbimpgVD  45256  hbalgVD  45257  hbexgVD  45258  ax6e2eqVD  45259  ax6e2ndVD  45260  ax6e2ndeqVD  45261  2sb5ndVD  45262  2uasbanhVD  45263  e2ebindVD  45264  sb5ALTVD  45265  vk15.4jVD  45266  notnotrALTVD  45267  con3ALTVD  45268