Theorem in1 44927

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

Syntax hints:   → wi 4  (   wvd1 44925

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 44926

This theorem is referenced by:  vd12  44956  vd13  44957  gen11nv  44973  gen12  44974  exinst11  44982  e1a  44983  el1  44984  e223  44991  e111  45030  e1111  45031  el2122old  45074  el12  45081  el123  45119  un0.1  45134  trsspwALT  45173  sspwtr  45176  pwtrVD  45179  pwtrrVD  45180  snssiALTVD  45182  snsslVD  45184  snelpwrVD  45186  unipwrVD  45187  sstrALT2VD  45189  suctrALT2VD  45191  elex2VD  45193  elex22VD  45194  eqsbc2VD  45195  zfregs2VD  45196  tpid3gVD  45197  en3lplem1VD  45198  en3lplem2VD  45199  en3lpVD  45200  3ornot23VD  45202  orbi1rVD  45203  3orbi123VD  45205  sbc3orgVD  45206  19.21a3con13vVD  45207  exbirVD  45208  exbiriVD  45209  rspsbc2VD  45210  3impexpVD  45211  3impexpbicomVD  45212  sbcoreleleqVD  45214  tratrbVD  45216  al2imVD  45217  syl5impVD  45218  ssralv2VD  45221  ordelordALTVD  45222  equncomVD  45223  imbi12VD  45228  imbi13VD  45229  sbcim2gVD  45230  sbcbiVD  45231  trsbcVD  45232  truniALTVD  45233  trintALTVD  45235  undif3VD  45237  sbcssgVD  45238  csbingVD  45239  simplbi2comtVD  45243  onfrALTVD  45246  csbeq2gVD  45247  csbsngVD  45248  csbxpgVD  45249  csbresgVD  45250  csbrngVD  45251  csbima12gALTVD  45252  csbunigVD  45253  csbfv12gALTVD  45254  con5VD  45255  relopabVD  45256  19.41rgVD  45257  2pm13.193VD  45258  hbimpgVD  45259  hbalgVD  45260  hbexgVD  45261  ax6e2eqVD  45262  ax6e2ndVD  45263  ax6e2ndeqVD  45264  2sb5ndVD  45265  2uasbanhVD  45266  e2ebindVD  45267  sb5ALTVD  45268  vk15.4jVD  45269  notnotrALTVD  45270  con3ALTVD  45271  sspwimpVD  45274  sspwimpcfVD  45276  suctrALTcfVD  45278