Theorem e1a 45227

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

Syntax hints:   → wi 4  (   wvd1 45169

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 45170

This theorem is referenced by:  e1bi  45229  e1bir  45230  snelpwrVD  45430  unipwrVD  45431  sstrALT2VD  45433  elex2VD  45437  elex22VD  45438  eqsbc2VD  45439  zfregs2VD  45440  tpid3gVD  45441  en3lplem1VD  45442  en3lpVD  45444  3ornot23VD  45446  3orbi123VD  45449  sbc3orgVD  45450  exbirVD  45452  3impexpVD  45455  3impexpbicomVD  45456  tratrbVD  45460  al2imVD  45461  syl5impVD  45462  ssralv2VD  45465  ordelordALTVD  45466  sbcim2gVD  45474  trsbcVD  45476  truniALTVD  45477  trintALTVD  45479  undif3VD  45481  sbcssgVD  45482  csbingVD  45483  onfrALTlem3VD  45486  simplbi2comtVD  45487  onfrALTlem2VD  45488  onfrALTVD  45490  csbeq2gVD  45491  csbsngVD  45492  csbxpgVD  45493  csbresgVD  45494  csbrngVD  45495  csbima12gALTVD  45496  csbunigVD  45497  csbfv12gALTVD  45498  con5VD  45499  relopabVD  45500  19.41rgVD  45501  2pm13.193VD  45502  hbimpgVD  45503  hbalgVD  45504  hbexgVD  45505  ax6e2eqVD  45506  ax6e2ndVD  45507  ax6e2ndeqVD  45508  2sb5ndVD  45509  2uasbanhVD  45510  e2ebindVD  45511  sb5ALTVD  45512  vk15.4jVD  45513  notnotrALTVD  45514  con3ALTVD  45515