Theorem e1a 45195

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

Syntax hints:   → wi 4  (   wvd1 45137

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 210  df-vd1 45138

This theorem is referenced by:  e1bi  45197  e1bir  45198  snelpwrVD  45398  unipwrVD  45399  sstrALT2VD  45401  elex2VD  45405  elex22VD  45406  eqsbc2VD  45407  zfregs2VD  45408  tpid3gVD  45409  en3lplem1VD  45410  en3lpVD  45412  3ornot23VD  45414  3orbi123VD  45417  sbc3orgVD  45418  exbirVD  45420  3impexpVD  45423  3impexpbicomVD  45424  tratrbVD  45428  al2imVD  45429  syl5impVD  45430  ssralv2VD  45433  ordelordALTVD  45434  sbcim2gVD  45442  trsbcVD  45444  truniALTVD  45445  trintALTVD  45447  undif3VD  45449  sbcssgVD  45450  csbingVD  45451  onfrALTlem3VD  45454  simplbi2comtVD  45455  onfrALTlem2VD  45456  onfrALTVD  45458  csbeq2gVD  45459  csbsngVD  45460  csbxpgVD  45461  csbresgVD  45462  csbrngVD  45463  csbima12gALTVD  45464  csbunigVD  45465  csbfv12gALTVD  45466  con5VD  45467  relopabVD  45468  19.41rgVD  45469  2pm13.193VD  45470  hbimpgVD  45471  hbalgVD  45472  hbexgVD  45473  ax6e2eqVD  45474  ax6e2ndVD  45475  ax6e2ndeqVD  45476  2sb5ndVD  45477  2uasbanhVD  45478  e2ebindVD  45479  sb5ALTVD  45480  vk15.4jVD  45481  notnotrALTVD  45482  con3ALTVD  45483