Theorem in1 44563

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

Syntax hints:   → wi 4  (   wvd1 44561

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 44562

This theorem is referenced by:  vd12  44592  vd13  44593  gen11nv  44609  gen12  44610  exinst11  44618  e1a  44619  el1  44620  e223  44627  e111  44666  e1111  44667  el2122old  44710  el12  44717  el123  44755  un0.1  44770  trsspwALT  44809  sspwtr  44812  pwtrVD  44815  pwtrrVD  44816  snssiALTVD  44818  snsslVD  44820  snelpwrVD  44822  unipwrVD  44823  sstrALT2VD  44825  suctrALT2VD  44827  elex2VD  44829  elex22VD  44830  eqsbc2VD  44831  zfregs2VD  44832  tpid3gVD  44833  en3lplem1VD  44834  en3lplem2VD  44835  en3lpVD  44836  3ornot23VD  44838  orbi1rVD  44839  3orbi123VD  44841  sbc3orgVD  44842  19.21a3con13vVD  44843  exbirVD  44844  exbiriVD  44845  rspsbc2VD  44846  3impexpVD  44847  3impexpbicomVD  44848  sbcoreleleqVD  44850  tratrbVD  44852  al2imVD  44853  syl5impVD  44854  ssralv2VD  44857  ordelordALTVD  44858  equncomVD  44859  imbi12VD  44864  imbi13VD  44865  sbcim2gVD  44866  sbcbiVD  44867  trsbcVD  44868  truniALTVD  44869  trintALTVD  44871  undif3VD  44873  sbcssgVD  44874  csbingVD  44875  simplbi2comtVD  44879  onfrALTVD  44882  csbeq2gVD  44883  csbsngVD  44884  csbxpgVD  44885  csbresgVD  44886  csbrngVD  44887  csbima12gALTVD  44888  csbunigVD  44889  csbfv12gALTVD  44890  con5VD  44891  relopabVD  44892  19.41rgVD  44893  2pm13.193VD  44894  hbimpgVD  44895  hbalgVD  44896  hbexgVD  44897  ax6e2eqVD  44898  ax6e2ndVD  44899  ax6e2ndeqVD  44900  2sb5ndVD  44901  2uasbanhVD  44902  e2ebindVD  44903  sb5ALTVD  44904  vk15.4jVD  44905  notnotrALTVD  44906  con3ALTVD  44907  sspwimpVD  44910  sspwimpcfVD  44912  suctrALTcfVD  44914