Theorem in1 44998

Description: Inference form of df-vd1 44997. 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 44997	. 2 ⊢ ((   𝜑   ▶   𝜓   ) ↔ (𝜑 → 𝜓))
3	1, 2	mpbi 230	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4  (   wvd1 44996

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 207  df-vd1 44997

This theorem is referenced by:  vd12  45027  vd13  45028  gen11nv  45044  gen12  45045  exinst11  45053  e1a  45054  el1  45055  e223  45062  e111  45101  e1111  45102  el2122old  45145  el12  45152  el123  45190  un0.1  45205  trsspwALT  45244  sspwtr  45247  pwtrVD  45250  pwtrrVD  45251  snssiALTVD  45253  snsslVD  45255  snelpwrVD  45257  unipwrVD  45258  sstrALT2VD  45260  suctrALT2VD  45262  elex2VD  45264  elex22VD  45265  eqsbc2VD  45266  zfregs2VD  45267  tpid3gVD  45268  en3lplem1VD  45269  en3lplem2VD  45270  en3lpVD  45271  3ornot23VD  45273  orbi1rVD  45274  3orbi123VD  45276  sbc3orgVD  45277  19.21a3con13vVD  45278  exbirVD  45279  exbiriVD  45280  rspsbc2VD  45281  3impexpVD  45282  3impexpbicomVD  45283  sbcoreleleqVD  45285  tratrbVD  45287  al2imVD  45288  syl5impVD  45289  ssralv2VD  45292  ordelordALTVD  45293  equncomVD  45294  imbi12VD  45299  imbi13VD  45300  sbcim2gVD  45301  sbcbiVD  45302  trsbcVD  45303  truniALTVD  45304  trintALTVD  45306  undif3VD  45308  sbcssgVD  45309  csbingVD  45310  simplbi2comtVD  45314  onfrALTVD  45317  csbeq2gVD  45318  csbsngVD  45319  csbxpgVD  45320  csbresgVD  45321  csbrngVD  45322  csbima12gALTVD  45323  csbunigVD  45324  csbfv12gALTVD  45325  con5VD  45326  relopabVD  45327  19.41rgVD  45328  2pm13.193VD  45329  hbimpgVD  45330  hbalgVD  45331  hbexgVD  45332  ax6e2eqVD  45333  ax6e2ndVD  45334  ax6e2ndeqVD  45335  2sb5ndVD  45336  2uasbanhVD  45337  e2ebindVD  45338  sb5ALTVD  45339  vk15.4jVD  45340  notnotrALTVD  45341  con3ALTVD  45342  sspwimpVD  45345  sspwimpcfVD  45347  suctrALTcfVD  45349