Theorem e1a 45163

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

Syntax hints:   → wi 4  (   wvd1 45105

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 209  df-vd1 45106

This theorem is referenced by:  e1bi  45165  e1bir  45166  snelpwrVD  45366  unipwrVD  45367  sstrALT2VD  45369  elex2VD  45373  elex22VD  45374  eqsbc2VD  45375  zfregs2VD  45376  tpid3gVD  45377  en3lplem1VD  45378  en3lpVD  45380  3ornot23VD  45382  3orbi123VD  45385  sbc3orgVD  45386  exbirVD  45388  3impexpVD  45391  3impexpbicomVD  45392  tratrbVD  45396  al2imVD  45397  syl5impVD  45398  ssralv2VD  45401  ordelordALTVD  45402  sbcim2gVD  45410  trsbcVD  45412  truniALTVD  45413  trintALTVD  45415  undif3VD  45417  sbcssgVD  45418  csbingVD  45419  onfrALTlem3VD  45422  simplbi2comtVD  45423  onfrALTlem2VD  45424  onfrALTVD  45426  csbeq2gVD  45427  csbsngVD  45428  csbxpgVD  45429  csbresgVD  45430  csbrngVD  45431  csbima12gALTVD  45432  csbunigVD  45433  csbfv12gALTVD  45434  con5VD  45435  relopabVD  45436  19.41rgVD  45437  2pm13.193VD  45438  hbimpgVD  45439  hbalgVD  45440  hbexgVD  45441  ax6e2eqVD  45442  ax6e2ndVD  45443  ax6e2ndeqVD  45444  2sb5ndVD  45445  2uasbanhVD  45446  e2ebindVD  45447  sb5ALTVD  45448  vk15.4jVD  45449  notnotrALTVD  45450  con3ALTVD  45451