Theorem in1 45030

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

Syntax hints:   → wi 4  (   wvd1 45028

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 209  df-vd1 45029

This theorem is referenced by:  vd12  45059  vd13  45060  gen11nv  45076  gen12  45077  exinst11  45085  e1a  45086  el1  45087  e223  45094  e111  45133  e1111  45134  el2122old  45177  el12  45184  el123  45222  un0.1  45237  trsspwALT  45276  sspwtr  45279  pwtrVD  45282  pwtrrVD  45283  snssiALTVD  45285  snsslVD  45287  snelpwrVD  45289  unipwrVD  45290  sstrALT2VD  45292  suctrALT2VD  45294  elex2VD  45296  elex22VD  45297  eqsbc2VD  45298  zfregs2VD  45299  tpid3gVD  45300  en3lplem1VD  45301  en3lplem2VD  45302  en3lpVD  45303  3ornot23VD  45305  orbi1rVD  45306  3orbi123VD  45308  sbc3orgVD  45309  19.21a3con13vVD  45310  exbirVD  45311  exbiriVD  45312  rspsbc2VD  45313  3impexpVD  45314  3impexpbicomVD  45315  sbcoreleleqVD  45317  tratrbVD  45319  al2imVD  45320  syl5impVD  45321  ssralv2VD  45324  ordelordALTVD  45325  equncomVD  45326  imbi12VD  45331  imbi13VD  45332  sbcim2gVD  45333  sbcbiVD  45334  trsbcVD  45335  truniALTVD  45336  trintALTVD  45338  undif3VD  45340  sbcssgVD  45341  csbingVD  45342  simplbi2comtVD  45346  onfrALTVD  45349  csbeq2gVD  45350  csbsngVD  45351  csbxpgVD  45352  csbresgVD  45353  csbrngVD  45354  csbima12gALTVD  45355  csbunigVD  45356  csbfv12gALTVD  45357  con5VD  45358  relopabVD  45359  19.41rgVD  45360  2pm13.193VD  45361  hbimpgVD  45362  hbalgVD  45363  hbexgVD  45364  ax6e2eqVD  45365  ax6e2ndVD  45366  ax6e2ndeqVD  45367  2sb5ndVD  45368  2uasbanhVD  45369  e2ebindVD  45370  sb5ALTVD  45371  vk15.4jVD  45372  notnotrALTVD  45373  con3ALTVD  45374  sspwimpVD  45377  sspwimpcfVD  45379  suctrALTcfVD  45381