Theorem in1 45019

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

Syntax hints:   → wi 4  (   wvd1 45017

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 45018

This theorem is referenced by:  vd12  45048  vd13  45049  gen11nv  45065  gen12  45066  exinst11  45074  e1a  45075  el1  45076  e223  45083  e111  45122  e1111  45123  el2122old  45166  el12  45173  el123  45211  un0.1  45226  trsspwALT  45265  sspwtr  45268  pwtrVD  45271  pwtrrVD  45272  snssiALTVD  45274  snsslVD  45276  snelpwrVD  45278  unipwrVD  45279  sstrALT2VD  45281  suctrALT2VD  45283  elex2VD  45285  elex22VD  45286  eqsbc2VD  45287  zfregs2VD  45288  tpid3gVD  45289  en3lplem1VD  45290  en3lplem2VD  45291  en3lpVD  45292  3ornot23VD  45294  orbi1rVD  45295  3orbi123VD  45297  sbc3orgVD  45298  19.21a3con13vVD  45299  exbirVD  45300  exbiriVD  45301  rspsbc2VD  45302  3impexpVD  45303  3impexpbicomVD  45304  sbcoreleleqVD  45306  tratrbVD  45308  al2imVD  45309  syl5impVD  45310  ssralv2VD  45313  ordelordALTVD  45314  equncomVD  45315  imbi12VD  45320  imbi13VD  45321  sbcim2gVD  45322  sbcbiVD  45323  trsbcVD  45324  truniALTVD  45325  trintALTVD  45327  undif3VD  45329  sbcssgVD  45330  csbingVD  45331  simplbi2comtVD  45335  onfrALTVD  45338  csbeq2gVD  45339  csbsngVD  45340  csbxpgVD  45341  csbresgVD  45342  csbrngVD  45343  csbima12gALTVD  45344  csbunigVD  45345  csbfv12gALTVD  45346  con5VD  45347  relopabVD  45348  19.41rgVD  45349  2pm13.193VD  45350  hbimpgVD  45351  hbalgVD  45352  hbexgVD  45353  ax6e2eqVD  45354  ax6e2ndVD  45355  ax6e2ndeqVD  45356  2sb5ndVD  45357  2uasbanhVD  45358  e2ebindVD  45359  sb5ALTVD  45360  vk15.4jVD  45361  notnotrALTVD  45362  con3ALTVD  45363  sspwimpVD  45366  sspwimpcfVD  45368  suctrALTcfVD  45370