Theorem e1a 45569

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

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

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 45512

This theorem is used by:  e1bi  45571  e1bir  45572  snelpwrVD  45772  unipwrVD  45773  sstrALT2VD  45775  elex2VD  45779  elex22VD  45780  eqsbc2VD  45781  zfregs2VD  45782  tpid3gVD  45783  en3lplem1VD  45784  en3lpVD  45786  3ornot23VD  45788  3orbi123VD  45791  sbc3orgVD  45792  exbirVD  45794  3impexpVD  45797  3impexpbicomVD  45798  tratrbVD  45802  al2imVD  45803  syl5impVD  45804  ssralv2VD  45807  ordelordALTVD  45808  sbcim2gVD  45816  trsbcVD  45818  truniALTVD  45819  trintALTVD  45821  undif3VD  45823  sbcssgVD  45824  csbingVD  45825  onfrALTlem3VD  45828  simplbi2comtVD  45829  onfrALTlem2VD  45830  onfrALTVD  45832  csbeq2gVD  45833  csbsngVD  45834  csbxpgVD  45835  csbresgVD  45836  csbrngVD  45837  csbima12gALTVD  45838  csbunigVD  45839  csbfv12gALTVD  45840  con5VD  45841  relopabVD  45842  19.41rgVD  45843  2pm13.193VD  45844  hbimpgVD  45845  hbalgVD  45846  hbexgVD  45847  ax6e2eqVD  45848  ax6e2ndVD  45849  ax6e2ndeqVD  45850  2sb5ndVD  45851  2uasbanhVD  45852  e2ebindVD  45853  sb5ALTVD  45854  vk15.4jVD  45855  notnotrALTVD  45856  con3ALTVD  45857