Theorem in1 44612

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

Syntax hints:   → wi 4  (   wvd1 44610

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 44611

This theorem is referenced by:  vd12  44641  vd13  44642  gen11nv  44658  gen12  44659  exinst11  44667  e1a  44668  el1  44669  e223  44676  e111  44715  e1111  44716  el2122old  44759  el12  44766  el123  44804  un0.1  44819  trsspwALT  44858  sspwtr  44861  pwtrVD  44864  pwtrrVD  44865  snssiALTVD  44867  snsslVD  44869  snelpwrVD  44871  unipwrVD  44872  sstrALT2VD  44874  suctrALT2VD  44876  elex2VD  44878  elex22VD  44879  eqsbc2VD  44880  zfregs2VD  44881  tpid3gVD  44882  en3lplem1VD  44883  en3lplem2VD  44884  en3lpVD  44885  3ornot23VD  44887  orbi1rVD  44888  3orbi123VD  44890  sbc3orgVD  44891  19.21a3con13vVD  44892  exbirVD  44893  exbiriVD  44894  rspsbc2VD  44895  3impexpVD  44896  3impexpbicomVD  44897  sbcoreleleqVD  44899  tratrbVD  44901  al2imVD  44902  syl5impVD  44903  ssralv2VD  44906  ordelordALTVD  44907  equncomVD  44908  imbi12VD  44913  imbi13VD  44914  sbcim2gVD  44915  sbcbiVD  44916  trsbcVD  44917  truniALTVD  44918  trintALTVD  44920  undif3VD  44922  sbcssgVD  44923  csbingVD  44924  simplbi2comtVD  44928  onfrALTVD  44931  csbeq2gVD  44932  csbsngVD  44933  csbxpgVD  44934  csbresgVD  44935  csbrngVD  44936  csbima12gALTVD  44937  csbunigVD  44938  csbfv12gALTVD  44939  con5VD  44940  relopabVD  44941  19.41rgVD  44942  2pm13.193VD  44943  hbimpgVD  44944  hbalgVD  44945  hbexgVD  44946  ax6e2eqVD  44947  ax6e2ndVD  44948  ax6e2ndeqVD  44949  2sb5ndVD  44950  2uasbanhVD  44951  e2ebindVD  44952  sb5ALTVD  44953  vk15.4jVD  44954  notnotrALTVD  44955  con3ALTVD  44956  sspwimpVD  44959  sspwimpcfVD  44961  suctrALTcfVD  44963