Theorem e1a 45377

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

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

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 45320

This theorem is used by:  e1bi  45379  e1bir  45380  snelpwrVD  45580  unipwrVD  45581  sstrALT2VD  45583  elex2VD  45587  elex22VD  45588  eqsbc2VD  45589  zfregs2VD  45590  tpid3gVD  45591  en3lplem1VD  45592  en3lpVD  45594  3ornot23VD  45596  3orbi123VD  45599  sbc3orgVD  45600  exbirVD  45602  3impexpVD  45605  3impexpbicomVD  45606  tratrbVD  45610  al2imVD  45611  syl5impVD  45612  ssralv2VD  45615  ordelordALTVD  45616  sbcim2gVD  45624  trsbcVD  45626  truniALTVD  45627  trintALTVD  45629  undif3VD  45631  sbcssgVD  45632  csbingVD  45633  onfrALTlem3VD  45636  simplbi2comtVD  45637  onfrALTlem2VD  45638  onfrALTVD  45640  csbeq2gVD  45641  csbsngVD  45642  csbxpgVD  45643  csbresgVD  45644  csbrngVD  45645  csbima12gALTVD  45646  csbunigVD  45647  csbfv12gALTVD  45648  con5VD  45649  relopabVD  45650  19.41rgVD  45651  2pm13.193VD  45652  hbimpgVD  45653  hbalgVD  45654  hbexgVD  45655  ax6e2eqVD  45656  ax6e2ndVD  45657  ax6e2ndeqVD  45658  2sb5ndVD  45659  2uasbanhVD  45660  e2ebindVD  45661  sb5ALTVD  45662  vk15.4jVD  45663  notnotrALTVD  45664  con3ALTVD  45665