Theorem in1 38787

Description: Inference form of df-vd1 38786. Virtual deduction introduction rule of converting the virtual hypothesis of a 1-virtual hypothesis virtual deduction into an antecedent. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis

Ref	Expression
in1.1	⊢ (   𝜑   ▶   𝜓   )

Assertion

Ref	Expression
in1	⊢ (𝜑 → 𝜓)

Proof of Theorem in1

Step	Hyp	Ref	Expression
1		in1.1	. 2 ⊢ (   𝜑   ▶   𝜓   )
2		df-vd1 38786	. 2 ⊢ ((   𝜑   ▶   𝜓   ) ↔ (𝜑 → 𝜓))
3	1, 2	mpbi 220	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4  (   wvd1 38785

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 197  df-vd1 38786

This theorem is referenced by:  vd12  38825  vd13  38826  gen11nv  38842  gen12  38843  exinst11  38851  e1a  38852  el1  38853  e223  38860  e111  38899  e1111  38900  el2122old  38944  el12  38953  el123  38991  un0.1  39006  trsspwALT  39045  sspwtr  39048  pwtrVD  39059  pwtrrVD  39060  snssiALTVD  39062  snsslVD  39064  snelpwrVD  39066  unipwrVD  39067  sstrALT2VD  39069  suctrALT2VD  39071  elex2VD  39073  elex22VD  39074  eqsbc3rVD  39075  zfregs2VD  39076  tpid3gVD  39077  en3lplem1VD  39078  en3lplem2VD  39079  en3lpVD  39080  3ornot23VD  39082  orbi1rVD  39083  3orbi123VD  39085  sbc3orgVD  39086  19.21a3con13vVD  39087  exbirVD  39088  exbiriVD  39089  rspsbc2VD  39090  3impexpVD  39091  3impexpbicomVD  39092  sbcoreleleqVD  39095  tratrbVD  39097  al2imVD  39098  syl5impVD  39099  ssralv2VD  39102  ordelordALTVD  39103  equncomVD  39104  imbi12VD  39109  imbi13VD  39110  sbcim2gVD  39111  sbcbiVD  39112  trsbcVD  39113  truniALTVD  39114  trintALTVD  39116  undif3VD  39118  sbcssgVD  39119  csbingVD  39120  simplbi2comtVD  39124  onfrALTVD  39127  csbeq2gVD  39128  csbsngVD  39129  csbxpgVD  39130  csbresgVD  39131  csbrngVD  39132  csbima12gALTVD  39133  csbunigVD  39134  csbfv12gALTVD  39135  con5VD  39136  relopabVD  39137  19.41rgVD  39138  2pm13.193VD  39139  hbimpgVD  39140  hbalgVD  39141  hbexgVD  39142  ax6e2eqVD  39143  ax6e2ndVD  39144  ax6e2ndeqVD  39145  2sb5ndVD  39146  2uasbanhVD  39147  e2ebindVD  39148  sb5ALTVD  39149  vk15.4jVD  39150  notnotrALTVD  39151  con3ALTVD  39152  sspwimpVD  39155  sspwimpcfVD  39157  suctrALTcfVD  39159