Theorem in1 44548

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

Syntax hints:   → wi 4  (   wvd1 44546

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 44547

This theorem is referenced by:  vd12  44577  vd13  44578  gen11nv  44594  gen12  44595  exinst11  44603  e1a  44604  el1  44605  e223  44612  e111  44651  e1111  44652  el2122old  44696  el12  44703  el123  44741  un0.1  44756  trsspwALT  44795  sspwtr  44798  pwtrVD  44801  pwtrrVD  44802  snssiALTVD  44804  snsslVD  44806  snelpwrVD  44808  unipwrVD  44809  sstrALT2VD  44811  suctrALT2VD  44813  elex2VD  44815  elex22VD  44816  eqsbc2VD  44817  zfregs2VD  44818  tpid3gVD  44819  en3lplem1VD  44820  en3lplem2VD  44821  en3lpVD  44822  3ornot23VD  44824  orbi1rVD  44825  3orbi123VD  44827  sbc3orgVD  44828  19.21a3con13vVD  44829  exbirVD  44830  exbiriVD  44831  rspsbc2VD  44832  3impexpVD  44833  3impexpbicomVD  44834  sbcoreleleqVD  44836  tratrbVD  44838  al2imVD  44839  syl5impVD  44840  ssralv2VD  44843  ordelordALTVD  44844  equncomVD  44845  imbi12VD  44850  imbi13VD  44851  sbcim2gVD  44852  sbcbiVD  44853  trsbcVD  44854  truniALTVD  44855  trintALTVD  44857  undif3VD  44859  sbcssgVD  44860  csbingVD  44861  simplbi2comtVD  44865  onfrALTVD  44868  csbeq2gVD  44869  csbsngVD  44870  csbxpgVD  44871  csbresgVD  44872  csbrngVD  44873  csbima12gALTVD  44874  csbunigVD  44875  csbfv12gALTVD  44876  con5VD  44877  relopabVD  44878  19.41rgVD  44879  2pm13.193VD  44880  hbimpgVD  44881  hbalgVD  44882  hbexgVD  44883  ax6e2eqVD  44884  ax6e2ndVD  44885  ax6e2ndeqVD  44886  2sb5ndVD  44887  2uasbanhVD  44888  e2ebindVD  44889  sb5ALTVD  44890  vk15.4jVD  44891  notnotrALTVD  44892  con3ALTVD  44893  sspwimpVD  44896  sspwimpcfVD  44898  suctrALTcfVD  44900