Theorem in1 45015

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

Syntax hints:   → wi 4  (   wvd1 45013

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 208  df-vd1 45014

This theorem is referenced by:  vd12  45044  vd13  45045  gen11nv  45061  gen12  45062  exinst11  45070  e1a  45071  el1  45072  e223  45079  e111  45118  e1111  45119  el2122old  45162  el12  45169  el123  45207  un0.1  45222  trsspwALT  45261  sspwtr  45264  pwtrVD  45267  pwtrrVD  45268  snssiALTVD  45270  snsslVD  45272  snelpwrVD  45274  unipwrVD  45275  sstrALT2VD  45277  suctrALT2VD  45279  elex2VD  45281  elex22VD  45282  eqsbc2VD  45283  zfregs2VD  45284  tpid3gVD  45285  en3lplem1VD  45286  en3lplem2VD  45287  en3lpVD  45288  3ornot23VD  45290  orbi1rVD  45291  3orbi123VD  45293  sbc3orgVD  45294  19.21a3con13vVD  45295  exbirVD  45296  exbiriVD  45297  rspsbc2VD  45298  3impexpVD  45299  3impexpbicomVD  45300  sbcoreleleqVD  45302  tratrbVD  45304  al2imVD  45305  syl5impVD  45306  ssralv2VD  45309  ordelordALTVD  45310  equncomVD  45311  imbi12VD  45316  imbi13VD  45317  sbcim2gVD  45318  sbcbiVD  45319  trsbcVD  45320  truniALTVD  45321  trintALTVD  45323  undif3VD  45325  sbcssgVD  45326  csbingVD  45327  simplbi2comtVD  45331  onfrALTVD  45334  csbeq2gVD  45335  csbsngVD  45336  csbxpgVD  45337  csbresgVD  45338  csbrngVD  45339  csbima12gALTVD  45340  csbunigVD  45341  csbfv12gALTVD  45342  con5VD  45343  relopabVD  45344  19.41rgVD  45345  2pm13.193VD  45346  hbimpgVD  45347  hbalgVD  45348  hbexgVD  45349  ax6e2eqVD  45350  ax6e2ndVD  45351  ax6e2ndeqVD  45352  2sb5ndVD  45353  2uasbanhVD  45354  e2ebindVD  45355  sb5ALTVD  45356  vk15.4jVD  45357  notnotrALTVD  45358  con3ALTVD  45359  sspwimpVD  45362  sspwimpcfVD  45364  suctrALTcfVD  45366