Theorem e1a 40954

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

Syntax hints:   → wi 4  (   wvd1 40896

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 209  df-vd1 40897

This theorem is referenced by:  e1bi  40956  e1bir  40957  snelpwrVD  41158  unipwrVD  41159  sstrALT2VD  41161  elex2VD  41165  elex22VD  41166  eqsbc3rVD  41167  zfregs2VD  41168  tpid3gVD  41169  en3lplem1VD  41170  en3lpVD  41172  3ornot23VD  41174  3orbi123VD  41177  sbc3orgVD  41178  exbirVD  41180  3impexpVD  41183  3impexpbicomVD  41184  tratrbVD  41188  al2imVD  41189  syl5impVD  41190  ssralv2VD  41193  ordelordALTVD  41194  sbcim2gVD  41202  trsbcVD  41204  truniALTVD  41205  trintALTVD  41207  undif3VD  41209  sbcssgVD  41210  csbingVD  41211  onfrALTlem3VD  41214  simplbi2comtVD  41215  onfrALTlem2VD  41216  onfrALTVD  41218  csbeq2gVD  41219  csbsngVD  41220  csbxpgVD  41221  csbresgVD  41222  csbrngVD  41223  csbima12gALTVD  41224  csbunigVD  41225  csbfv12gALTVD  41226  con5VD  41227  relopabVD  41228  19.41rgVD  41229  2pm13.193VD  41230  hbimpgVD  41231  hbalgVD  41232  hbexgVD  41233  ax6e2eqVD  41234  ax6e2ndVD  41235  ax6e2ndeqVD  41236  2sb5ndVD  41237  2uasbanhVD  41238  e2ebindVD  41239  sb5ALTVD  41240  vk15.4jVD  41241  notnotrALTVD  41242  con3ALTVD  41243