Theorem in1 44001

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

Syntax hints:   → wi 4  (   wvd1 43999

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 206  df-vd1 44000

This theorem is referenced by:  vd12  44030  vd13  44031  gen11nv  44047  gen12  44048  exinst11  44056  e1a  44057  el1  44058  e223  44065  e111  44104  e1111  44105  el2122old  44149  el12  44156  el123  44194  un0.1  44209  trsspwALT  44248  sspwtr  44251  pwtrVD  44254  pwtrrVD  44255  snssiALTVD  44257  snsslVD  44259  snelpwrVD  44261  unipwrVD  44262  sstrALT2VD  44264  suctrALT2VD  44266  elex2VD  44268  elex22VD  44269  eqsbc2VD  44270  zfregs2VD  44271  tpid3gVD  44272  en3lplem1VD  44273  en3lplem2VD  44274  en3lpVD  44275  3ornot23VD  44277  orbi1rVD  44278  3orbi123VD  44280  sbc3orgVD  44281  19.21a3con13vVD  44282  exbirVD  44283  exbiriVD  44284  rspsbc2VD  44285  3impexpVD  44286  3impexpbicomVD  44287  sbcoreleleqVD  44289  tratrbVD  44291  al2imVD  44292  syl5impVD  44293  ssralv2VD  44296  ordelordALTVD  44297  equncomVD  44298  imbi12VD  44303  imbi13VD  44304  sbcim2gVD  44305  sbcbiVD  44306  trsbcVD  44307  truniALTVD  44308  trintALTVD  44310  undif3VD  44312  sbcssgVD  44313  csbingVD  44314  simplbi2comtVD  44318  onfrALTVD  44321  csbeq2gVD  44322  csbsngVD  44323  csbxpgVD  44324  csbresgVD  44325  csbrngVD  44326  csbima12gALTVD  44327  csbunigVD  44328  csbfv12gALTVD  44329  con5VD  44330  relopabVD  44331  19.41rgVD  44332  2pm13.193VD  44333  hbimpgVD  44334  hbalgVD  44335  hbexgVD  44336  ax6e2eqVD  44337  ax6e2ndVD  44338  ax6e2ndeqVD  44339  2sb5ndVD  44340  2uasbanhVD  44341  e2ebindVD  44342  sb5ALTVD  44343  vk15.4jVD  44344  notnotrALTVD  44345  con3ALTVD  44346  sspwimpVD  44349  sspwimpcfVD  44351  suctrALTcfVD  44353