Theorem in1 44569

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

Syntax hints:   → wi 4  (   wvd1 44567

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 44568

This theorem is referenced by:  vd12  44598  vd13  44599  gen11nv  44615  gen12  44616  exinst11  44624  e1a  44625  el1  44626  e223  44633  e111  44672  e1111  44673  el2122old  44717  el12  44724  el123  44762  un0.1  44777  trsspwALT  44816  sspwtr  44819  pwtrVD  44822  pwtrrVD  44823  snssiALTVD  44825  snsslVD  44827  snelpwrVD  44829  unipwrVD  44830  sstrALT2VD  44832  suctrALT2VD  44834  elex2VD  44836  elex22VD  44837  eqsbc2VD  44838  zfregs2VD  44839  tpid3gVD  44840  en3lplem1VD  44841  en3lplem2VD  44842  en3lpVD  44843  3ornot23VD  44845  orbi1rVD  44846  3orbi123VD  44848  sbc3orgVD  44849  19.21a3con13vVD  44850  exbirVD  44851  exbiriVD  44852  rspsbc2VD  44853  3impexpVD  44854  3impexpbicomVD  44855  sbcoreleleqVD  44857  tratrbVD  44859  al2imVD  44860  syl5impVD  44861  ssralv2VD  44864  ordelordALTVD  44865  equncomVD  44866  imbi12VD  44871  imbi13VD  44872  sbcim2gVD  44873  sbcbiVD  44874  trsbcVD  44875  truniALTVD  44876  trintALTVD  44878  undif3VD  44880  sbcssgVD  44881  csbingVD  44882  simplbi2comtVD  44886  onfrALTVD  44889  csbeq2gVD  44890  csbsngVD  44891  csbxpgVD  44892  csbresgVD  44893  csbrngVD  44894  csbima12gALTVD  44895  csbunigVD  44896  csbfv12gALTVD  44897  con5VD  44898  relopabVD  44899  19.41rgVD  44900  2pm13.193VD  44901  hbimpgVD  44902  hbalgVD  44903  hbexgVD  44904  ax6e2eqVD  44905  ax6e2ndVD  44906  ax6e2ndeqVD  44907  2sb5ndVD  44908  2uasbanhVD  44909  e2ebindVD  44910  sb5ALTVD  44911  vk15.4jVD  44912  notnotrALTVD  44913  con3ALTVD  44914  sspwimpVD  44917  sspwimpcfVD  44919  suctrALTcfVD  44921