Theorem e1a 45458

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

This proof depends on syntax axioms:   → wi 4  (   wvd1 45400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-vd1 45401

This theorem is used by:  e1bi  45460  e1bir  45461  snelpwrVD  45661  unipwrVD  45662  sstrALT2VD  45664  elex2VD  45668  elex22VD  45669  eqsbc2VD  45670  zfregs2VD  45671  tpid3gVD  45672  en3lplem1VD  45673  en3lpVD  45675  3ornot23VD  45677  3orbi123VD  45680  sbc3orgVD  45681  exbirVD  45683  3impexpVD  45686  3impexpbicomVD  45687  tratrbVD  45691  al2imVD  45692  syl5impVD  45693  ssralv2VD  45696  ordelordALTVD  45697  sbcim2gVD  45705  trsbcVD  45707  truniALTVD  45708  trintALTVD  45710  undif3VD  45712  sbcssgVD  45713  csbingVD  45714  onfrALTlem3VD  45717  simplbi2comtVD  45718  onfrALTlem2VD  45719  onfrALTVD  45721  csbeq2gVD  45722  csbsngVD  45723  csbxpgVD  45724  csbresgVD  45725  csbrngVD  45726  csbima12gALTVD  45727  csbunigVD  45728  csbfv12gALTVD  45729  con5VD  45730  relopabVD  45731  19.41rgVD  45732  2pm13.193VD  45733  hbimpgVD  45734  hbalgVD  45735  hbexgVD  45736  ax6e2eqVD  45737  ax6e2ndVD  45738  ax6e2ndeqVD  45739  2sb5ndVD  45740  2uasbanhVD  45741  e2ebindVD  45742  sb5ALTVD  45743  vk15.4jVD  45744  notnotrALTVD  45745  con3ALTVD  45746