Theorem e1a 37873

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

Syntax hints:   → wi 4  (   wvd1 37806

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 196  df-vd1 37807

This theorem is referenced by:  e1bi  37875  e1bir  37876  snelpwrVD  38088  unipwrVD  38089  sstrALT2VD  38091  elex2VD  38095  elex22VD  38096  eqsbc3rVD  38097  zfregs2VD  38098  tpid3gVD  38099  en3lplem1VD  38100  en3lpVD  38102  3ornot23VD  38104  3orbi123VD  38107  sbc3orgVD  38108  exbirVD  38110  3impexpVD  38113  3impexpbicomVD  38114  sbcoreleleqVD  38117  tratrbVD  38119  al2imVD  38120  syl5impVD  38121  ssralv2VD  38124  ordelordALTVD  38125  sbcim2gVD  38133  trsbcVD  38135  truniALTVD  38136  trintALTVD  38138  undif3VD  38140  sbcssgVD  38141  csbingVD  38142  onfrALTlem3VD  38145  simplbi2comtVD  38146  onfrALTlem2VD  38147  onfrALTVD  38149  csbeq2gVD  38150  csbsngVD  38151  csbxpgVD  38152  csbresgVD  38153  csbrngVD  38154  csbima12gALTVD  38155  csbunigVD  38156  csbfv12gALTVD  38157  con5VD  38158  relopabVD  38159  19.41rgVD  38160  2pm13.193VD  38161  hbimpgVD  38162  hbalgVD  38163  hbexgVD  38164  ax6e2eqVD  38165  ax6e2ndVD  38166  ax6e2ndeqVD  38167  2sb5ndVD  38168  2uasbanhVD  38169  e2ebindVD  38170  sb5ALTVD  38171  vk15.4jVD  38172  notnotrALTVD  38173  con3ALTVD  38174