Theorem in1 44754

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

Syntax hints:   → wi 4  (   wvd1 44752

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 44753

This theorem is referenced by:  vd12  44783  vd13  44784  gen11nv  44800  gen12  44801  exinst11  44809  e1a  44810  el1  44811  e223  44818  e111  44857  e1111  44858  el2122old  44901  el12  44908  el123  44946  un0.1  44961  trsspwALT  45000  sspwtr  45003  pwtrVD  45006  pwtrrVD  45007  snssiALTVD  45009  snsslVD  45011  snelpwrVD  45013  unipwrVD  45014  sstrALT2VD  45016  suctrALT2VD  45018  elex2VD  45020  elex22VD  45021  eqsbc2VD  45022  zfregs2VD  45023  tpid3gVD  45024  en3lplem1VD  45025  en3lplem2VD  45026  en3lpVD  45027  3ornot23VD  45029  orbi1rVD  45030  3orbi123VD  45032  sbc3orgVD  45033  19.21a3con13vVD  45034  exbirVD  45035  exbiriVD  45036  rspsbc2VD  45037  3impexpVD  45038  3impexpbicomVD  45039  sbcoreleleqVD  45041  tratrbVD  45043  al2imVD  45044  syl5impVD  45045  ssralv2VD  45048  ordelordALTVD  45049  equncomVD  45050  imbi12VD  45055  imbi13VD  45056  sbcim2gVD  45057  sbcbiVD  45058  trsbcVD  45059  truniALTVD  45060  trintALTVD  45062  undif3VD  45064  sbcssgVD  45065  csbingVD  45066  simplbi2comtVD  45070  onfrALTVD  45073  csbeq2gVD  45074  csbsngVD  45075  csbxpgVD  45076  csbresgVD  45077  csbrngVD  45078  csbima12gALTVD  45079  csbunigVD  45080  csbfv12gALTVD  45081  con5VD  45082  relopabVD  45083  19.41rgVD  45084  2pm13.193VD  45085  hbimpgVD  45086  hbalgVD  45087  hbexgVD  45088  ax6e2eqVD  45089  ax6e2ndVD  45090  ax6e2ndeqVD  45091  2sb5ndVD  45092  2uasbanhVD  45093  e2ebindVD  45094  sb5ALTVD  45095  vk15.4jVD  45096  notnotrALTVD  45097  con3ALTVD  45098  sspwimpVD  45101  sspwimpcfVD  45103  suctrALTcfVD  45105