Theorem in1 44554

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

Syntax hints:   → wi 4  (   wvd1 44552

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 44553

This theorem is referenced by:  vd12  44583  vd13  44584  gen11nv  44600  gen12  44601  exinst11  44609  e1a  44610  el1  44611  e223  44618  e111  44657  e1111  44658  el2122old  44701  el12  44708  el123  44746  un0.1  44761  trsspwALT  44800  sspwtr  44803  pwtrVD  44806  pwtrrVD  44807  snssiALTVD  44809  snsslVD  44811  snelpwrVD  44813  unipwrVD  44814  sstrALT2VD  44816  suctrALT2VD  44818  elex2VD  44820  elex22VD  44821  eqsbc2VD  44822  zfregs2VD  44823  tpid3gVD  44824  en3lplem1VD  44825  en3lplem2VD  44826  en3lpVD  44827  3ornot23VD  44829  orbi1rVD  44830  3orbi123VD  44832  sbc3orgVD  44833  19.21a3con13vVD  44834  exbirVD  44835  exbiriVD  44836  rspsbc2VD  44837  3impexpVD  44838  3impexpbicomVD  44839  sbcoreleleqVD  44841  tratrbVD  44843  al2imVD  44844  syl5impVD  44845  ssralv2VD  44848  ordelordALTVD  44849  equncomVD  44850  imbi12VD  44855  imbi13VD  44856  sbcim2gVD  44857  sbcbiVD  44858  trsbcVD  44859  truniALTVD  44860  trintALTVD  44862  undif3VD  44864  sbcssgVD  44865  csbingVD  44866  simplbi2comtVD  44870  onfrALTVD  44873  csbeq2gVD  44874  csbsngVD  44875  csbxpgVD  44876  csbresgVD  44877  csbrngVD  44878  csbima12gALTVD  44879  csbunigVD  44880  csbfv12gALTVD  44881  con5VD  44882  relopabVD  44883  19.41rgVD  44884  2pm13.193VD  44885  hbimpgVD  44886  hbalgVD  44887  hbexgVD  44888  ax6e2eqVD  44889  ax6e2ndVD  44890  ax6e2ndeqVD  44891  2sb5ndVD  44892  2uasbanhVD  44893  e2ebindVD  44894  sb5ALTVD  44895  vk15.4jVD  44896  notnotrALTVD  44897  con3ALTVD  44898  sspwimpVD  44901  sspwimpcfVD  44903  suctrALTcfVD  44905