Theorem e1_ 16518

Description: A Virtual deduction elimination rule. syl 12 is e1_ 16518 without virtual deductions.

Hypotheses

Ref	Expression
e1_.1	|- . ph   ⊢   ps .
e1_.2	|- (ps -> ch)

Assertion

Ref	Expression
e1_	|- . ph   ⊢   ch .

Proof of Theorem e1_

Step	Hyp	Ref	Expression
1		e1_.1	. . . 4 |- . ph   ⊢   ps .
2	1	in1 16481	. . 3 |- (ph -> ps)
3		e1_.2	. . 3 |- (ps -> ch)
4	2, 3	syl 12	. 2 |- (ph -> ch)
5	4	dfvd1ir 16483	1 |- . ph   ⊢   ch .

Syntax hints:   -> wi 3   . vd1 16479

This theorem is referenced by:  e1bi 16519  e1bir 16520  snelpwrVD 16654  unipwrVD 16656  sstrALT2VD 16658  elex2VD 16662  elex22VD 16663  eqsbc3rVD 16664  zfregs2VD 16665  tpid3gVD 16666  en3lplem1VD 16667  en3lpVD 16669  3ornot23VD 16671  bitr3VD 16673  3orbi123VD 16674  sbc3orgVD 16675  exbirVD 16677  3impexpVD 16680  3impexpbicomVD 16681  sbcoreleleqVD 16683  tratrbVD 16685  3ax5VD 16686  syl5impVD 16687  ssralv2VD 16690  ordelordaxrVD 16691  sbcim2gVD 16699  trsbcVD 16701  truniALTVD 16702  trintALTVD 16704  undif3VD 16706

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-vd1 16480

Copyright terms: Public domain