Theorem in1 44812

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

Syntax hints:   → wi 4  (   wvd1 44810

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 44811

This theorem is referenced by:  vd12  44841  vd13  44842  gen11nv  44858  gen12  44859  exinst11  44867  e1a  44868  el1  44869  e223  44876  e111  44915  e1111  44916  el2122old  44959  el12  44966  el123  45004  un0.1  45019  trsspwALT  45058  sspwtr  45061  pwtrVD  45064  pwtrrVD  45065  snssiALTVD  45067  snsslVD  45069  snelpwrVD  45071  unipwrVD  45072  sstrALT2VD  45074  suctrALT2VD  45076  elex2VD  45078  elex22VD  45079  eqsbc2VD  45080  zfregs2VD  45081  tpid3gVD  45082  en3lplem1VD  45083  en3lplem2VD  45084  en3lpVD  45085  3ornot23VD  45087  orbi1rVD  45088  3orbi123VD  45090  sbc3orgVD  45091  19.21a3con13vVD  45092  exbirVD  45093  exbiriVD  45094  rspsbc2VD  45095  3impexpVD  45096  3impexpbicomVD  45097  sbcoreleleqVD  45099  tratrbVD  45101  al2imVD  45102  syl5impVD  45103  ssralv2VD  45106  ordelordALTVD  45107  equncomVD  45108  imbi12VD  45113  imbi13VD  45114  sbcim2gVD  45115  sbcbiVD  45116  trsbcVD  45117  truniALTVD  45118  trintALTVD  45120  undif3VD  45122  sbcssgVD  45123  csbingVD  45124  simplbi2comtVD  45128  onfrALTVD  45131  csbeq2gVD  45132  csbsngVD  45133  csbxpgVD  45134  csbresgVD  45135  csbrngVD  45136  csbima12gALTVD  45137  csbunigVD  45138  csbfv12gALTVD  45139  con5VD  45140  relopabVD  45141  19.41rgVD  45142  2pm13.193VD  45143  hbimpgVD  45144  hbalgVD  45145  hbexgVD  45146  ax6e2eqVD  45147  ax6e2ndVD  45148  ax6e2ndeqVD  45149  2sb5ndVD  45150  2uasbanhVD  45151  e2ebindVD  45152  sb5ALTVD  45153  vk15.4jVD  45154  notnotrALTVD  45155  con3ALTVD  45156  sspwimpVD  45159  sspwimpcfVD  45161  suctrALTcfVD  45163