Theorem in1 45662

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

This proof depends on syntax axioms:   → wi 4  (   wvd1 45660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-vd1 45661

This theorem is used by:  vd12  45691  vd13  45692  gen11nv  45708  gen12  45709  exinst11  45717  e1a  45718  el1  45719  e223  45726  e111  45765  e1111  45766  el2122old  45809  el12  45816  el123  45854  un0.1  45869  trsspwALT  45908  sspwtr  45911  pwtrVD  45914  pwtrrVD  45915  snssiALTVD  45917  snsslVD  45919  snelpwrVD  45921  unipwrVD  45922  sstrALT2VD  45924  suctrALT2VD  45926  elex2VD  45928  elex22VD  45929  eqsbc2VD  45930  zfregs2VD  45931  tpid3gVD  45932  en3lplem1VD  45933  en3lplem2VD  45934  en3lpVD  45935  3ornot23VD  45937  orbi1rVD  45938  3orbi123VD  45940  sbc3orgVD  45941  19.21a3con13vVD  45942  exbirVD  45943  exbiriVD  45944  rspsbc2VD  45945  3impexpVD  45946  3impexpbicomVD  45947  sbcoreleleqVD  45949  tratrbVD  45951  al2imVD  45952  syl5impVD  45953  ssralv2VD  45956  ordelordALTVD  45957  equncomVD  45958  imbi12VD  45963  imbi13VD  45964  sbcim2gVD  45965  sbcbiVD  45966  trsbcVD  45967  truniALTVD  45968  trintALTVD  45970  undif3VD  45972  sbcssgVD  45973  csbingVD  45974  simplbi2comtVD  45978  onfrALTVD  45981  csbeq2gVD  45982  csbsngVD  45983  csbxpgVD  45984  csbresgVD  45985  csbrngVD  45986  csbima12gALTVD  45987  csbunigVD  45988  csbfv12gALTVD  45989  con5VD  45990  relopabVD  45991  19.41rgVD  45992  2pm13.193VD  45993  hbimpgVD  45994  hbalgVD  45995  hbexgVD  45996  ax6e2eqVD  45997  ax6e2ndVD  45998  ax6e2ndeqVD  45999  2sb5ndVD  46000  2uasbanhVD  46001  e2ebindVD  46002  sb5ALTVD  46003  vk15.4jVD  46004  notnotrALTVD  46005  con3ALTVD  46006  sspwimpVD  46009  sspwimpcfVD  46011  suctrALTcfVD  46013