Theorem in1 44596

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

Syntax hints:   → wi 4  (   wvd1 44594

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 44595

This theorem is referenced by:  vd12  44625  vd13  44626  gen11nv  44642  gen12  44643  exinst11  44651  e1a  44652  el1  44653  e223  44660  e111  44699  e1111  44700  el2122old  44744  el12  44751  el123  44789  un0.1  44804  trsspwALT  44843  sspwtr  44846  pwtrVD  44849  pwtrrVD  44850  snssiALTVD  44852  snsslVD  44854  snelpwrVD  44856  unipwrVD  44857  sstrALT2VD  44859  suctrALT2VD  44861  elex2VD  44863  elex22VD  44864  eqsbc2VD  44865  zfregs2VD  44866  tpid3gVD  44867  en3lplem1VD  44868  en3lplem2VD  44869  en3lpVD  44870  3ornot23VD  44872  orbi1rVD  44873  3orbi123VD  44875  sbc3orgVD  44876  19.21a3con13vVD  44877  exbirVD  44878  exbiriVD  44879  rspsbc2VD  44880  3impexpVD  44881  3impexpbicomVD  44882  sbcoreleleqVD  44884  tratrbVD  44886  al2imVD  44887  syl5impVD  44888  ssralv2VD  44891  ordelordALTVD  44892  equncomVD  44893  imbi12VD  44898  imbi13VD  44899  sbcim2gVD  44900  sbcbiVD  44901  trsbcVD  44902  truniALTVD  44903  trintALTVD  44905  undif3VD  44907  sbcssgVD  44908  csbingVD  44909  simplbi2comtVD  44913  onfrALTVD  44916  csbeq2gVD  44917  csbsngVD  44918  csbxpgVD  44919  csbresgVD  44920  csbrngVD  44921  csbima12gALTVD  44922  csbunigVD  44923  csbfv12gALTVD  44924  con5VD  44925  relopabVD  44926  19.41rgVD  44927  2pm13.193VD  44928  hbimpgVD  44929  hbalgVD  44930  hbexgVD  44931  ax6e2eqVD  44932  ax6e2ndVD  44933  ax6e2ndeqVD  44934  2sb5ndVD  44935  2uasbanhVD  44936  e2ebindVD  44937  sb5ALTVD  44938  vk15.4jVD  44939  notnotrALTVD  44940  con3ALTVD  44941  sspwimpVD  44944  sspwimpcfVD  44946  suctrALTcfVD  44948