Theorem in1 40463

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

Syntax hints:   → wi 4  (   wvd1 40461

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 40462

This theorem is referenced by:  vd12  40492  vd13  40493  gen11nv  40509  gen12  40510  exinst11  40518  e1a  40519  el1  40520  e223  40527  e111  40566  e1111  40567  el2122old  40611  el12  40618  el123  40656  un0.1  40671  trsspwALT  40710  sspwtr  40713  pwtrVD  40716  pwtrrVD  40717  snssiALTVD  40719  snsslVD  40721  snelpwrVD  40723  unipwrVD  40724  sstrALT2VD  40726  suctrALT2VD  40728  elex2VD  40730  elex22VD  40731  eqsbc3rVD  40732  zfregs2VD  40733  tpid3gVD  40734  en3lplem1VD  40735  en3lplem2VD  40736  en3lpVD  40737  3ornot23VD  40739  orbi1rVD  40740  3orbi123VD  40742  sbc3orgVD  40743  19.21a3con13vVD  40744  exbirVD  40745  exbiriVD  40746  rspsbc2VD  40747  3impexpVD  40748  3impexpbicomVD  40749  sbcoreleleqVD  40751  tratrbVD  40753  al2imVD  40754  syl5impVD  40755  ssralv2VD  40758  ordelordALTVD  40759  equncomVD  40760  imbi12VD  40765  imbi13VD  40766  sbcim2gVD  40767  sbcbiVD  40768  trsbcVD  40769  truniALTVD  40770  trintALTVD  40772  undif3VD  40774  sbcssgVD  40775  csbingVD  40776  simplbi2comtVD  40780  onfrALTVD  40783  csbeq2gVD  40784  csbsngVD  40785  csbxpgVD  40786  csbresgVD  40787  csbrngVD  40788  csbima12gALTVD  40789  csbunigVD  40790  csbfv12gALTVD  40791  con5VD  40792  relopabVD  40793  19.41rgVD  40794  2pm13.193VD  40795  hbimpgVD  40796  hbalgVD  40797  hbexgVD  40798  ax6e2eqVD  40799  ax6e2ndVD  40800  ax6e2ndeqVD  40801  2sb5ndVD  40802  2uasbanhVD  40803  e2ebindVD  40804  sb5ALTVD  40805  vk15.4jVD  40806  notnotrALTVD  40807  con3ALTVD  40808  sspwimpVD  40811  sspwimpcfVD  40813  suctrALTcfVD  40815