Theorem in1 44545

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

Syntax hints:   → wi 4  (   wvd1 44543

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 44544

This theorem is referenced by:  vd12  44574  vd13  44575  gen11nv  44591  gen12  44592  exinst11  44600  e1a  44601  el1  44602  e223  44609  e111  44648  e1111  44649  el2122old  44692  el12  44699  el123  44737  un0.1  44752  trsspwALT  44791  sspwtr  44794  pwtrVD  44797  pwtrrVD  44798  snssiALTVD  44800  snsslVD  44802  snelpwrVD  44804  unipwrVD  44805  sstrALT2VD  44807  suctrALT2VD  44809  elex2VD  44811  elex22VD  44812  eqsbc2VD  44813  zfregs2VD  44814  tpid3gVD  44815  en3lplem1VD  44816  en3lplem2VD  44817  en3lpVD  44818  3ornot23VD  44820  orbi1rVD  44821  3orbi123VD  44823  sbc3orgVD  44824  19.21a3con13vVD  44825  exbirVD  44826  exbiriVD  44827  rspsbc2VD  44828  3impexpVD  44829  3impexpbicomVD  44830  sbcoreleleqVD  44832  tratrbVD  44834  al2imVD  44835  syl5impVD  44836  ssralv2VD  44839  ordelordALTVD  44840  equncomVD  44841  imbi12VD  44846  imbi13VD  44847  sbcim2gVD  44848  sbcbiVD  44849  trsbcVD  44850  truniALTVD  44851  trintALTVD  44853  undif3VD  44855  sbcssgVD  44856  csbingVD  44857  simplbi2comtVD  44861  onfrALTVD  44864  csbeq2gVD  44865  csbsngVD  44866  csbxpgVD  44867  csbresgVD  44868  csbrngVD  44869  csbima12gALTVD  44870  csbunigVD  44871  csbfv12gALTVD  44872  con5VD  44873  relopabVD  44874  19.41rgVD  44875  2pm13.193VD  44876  hbimpgVD  44877  hbalgVD  44878  hbexgVD  44879  ax6e2eqVD  44880  ax6e2ndVD  44881  ax6e2ndeqVD  44882  2sb5ndVD  44883  2uasbanhVD  44884  e2ebindVD  44885  sb5ALTVD  44886  vk15.4jVD  44887  notnotrALTVD  44888  con3ALTVD  44889  sspwimpVD  44892  sspwimpcfVD  44894  suctrALTcfVD  44896