Theorem in1 44561

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

Syntax hints:   → wi 4  (   wvd1 44559

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 44560

This theorem is referenced by:  vd12  44590  vd13  44591  gen11nv  44607  gen12  44608  exinst11  44616  e1a  44617  el1  44618  e223  44625  e111  44664  e1111  44665  el2122old  44708  el12  44715  el123  44753  un0.1  44768  trsspwALT  44807  sspwtr  44810  pwtrVD  44813  pwtrrVD  44814  snssiALTVD  44816  snsslVD  44818  snelpwrVD  44820  unipwrVD  44821  sstrALT2VD  44823  suctrALT2VD  44825  elex2VD  44827  elex22VD  44828  eqsbc2VD  44829  zfregs2VD  44830  tpid3gVD  44831  en3lplem1VD  44832  en3lplem2VD  44833  en3lpVD  44834  3ornot23VD  44836  orbi1rVD  44837  3orbi123VD  44839  sbc3orgVD  44840  19.21a3con13vVD  44841  exbirVD  44842  exbiriVD  44843  rspsbc2VD  44844  3impexpVD  44845  3impexpbicomVD  44846  sbcoreleleqVD  44848  tratrbVD  44850  al2imVD  44851  syl5impVD  44852  ssralv2VD  44855  ordelordALTVD  44856  equncomVD  44857  imbi12VD  44862  imbi13VD  44863  sbcim2gVD  44864  sbcbiVD  44865  trsbcVD  44866  truniALTVD  44867  trintALTVD  44869  undif3VD  44871  sbcssgVD  44872  csbingVD  44873  simplbi2comtVD  44877  onfrALTVD  44880  csbeq2gVD  44881  csbsngVD  44882  csbxpgVD  44883  csbresgVD  44884  csbrngVD  44885  csbima12gALTVD  44886  csbunigVD  44887  csbfv12gALTVD  44888  con5VD  44889  relopabVD  44890  19.41rgVD  44891  2pm13.193VD  44892  hbimpgVD  44893  hbalgVD  44894  hbexgVD  44895  ax6e2eqVD  44896  ax6e2ndVD  44897  ax6e2ndeqVD  44898  2sb5ndVD  44899  2uasbanhVD  44900  e2ebindVD  44901  sb5ALTVD  44902  vk15.4jVD  44903  notnotrALTVD  44904  con3ALTVD  44905  sspwimpVD  44908  sspwimpcfVD  44910  suctrALTcfVD  44912