Theorem in1 45539

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

This proof depends on syntax axioms:   → wi 4  (   wvd1 45537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-vd1 45538

This theorem is used by:  vd12  45568  vd13  45569  gen11nv  45585  gen12  45586  exinst11  45594  e1a  45595  el1  45596  e223  45603  e111  45642  e1111  45643  el2122old  45686  el12  45693  el123  45731  un0.1  45746  trsspwALT  45785  sspwtr  45788  pwtrVD  45791  pwtrrVD  45792  snssiALTVD  45794  snsslVD  45796  snelpwrVD  45798  unipwrVD  45799  sstrALT2VD  45801  suctrALT2VD  45803  elex2VD  45805  elex22VD  45806  eqsbc2VD  45807  zfregs2VD  45808  tpid3gVD  45809  en3lplem1VD  45810  en3lplem2VD  45811  en3lpVD  45812  3ornot23VD  45814  orbi1rVD  45815  3orbi123VD  45817  sbc3orgVD  45818  19.21a3con13vVD  45819  exbirVD  45820  exbiriVD  45821  rspsbc2VD  45822  3impexpVD  45823  3impexpbicomVD  45824  sbcoreleleqVD  45826  tratrbVD  45828  al2imVD  45829  syl5impVD  45830  ssralv2VD  45833  ordelordALTVD  45834  equncomVD  45835  imbi12VD  45840  imbi13VD  45841  sbcim2gVD  45842  sbcbiVD  45843  trsbcVD  45844  truniALTVD  45845  trintALTVD  45847  undif3VD  45849  sbcssgVD  45850  csbingVD  45851  simplbi2comtVD  45855  onfrALTVD  45858  csbeq2gVD  45859  csbsngVD  45860  csbxpgVD  45861  csbresgVD  45862  csbrngVD  45863  csbima12gALTVD  45864  csbunigVD  45865  csbfv12gALTVD  45866  con5VD  45867  relopabVD  45868  19.41rgVD  45869  2pm13.193VD  45870  hbimpgVD  45871  hbalgVD  45872  hbexgVD  45873  ax6e2eqVD  45874  ax6e2ndVD  45875  ax6e2ndeqVD  45876  2sb5ndVD  45877  2uasbanhVD  45878  e2ebindVD  45879  sb5ALTVD  45880  vk15.4jVD  45881  notnotrALTVD  45882  con3ALTVD  45883  sspwimpVD  45886  sspwimpcfVD  45888  suctrALTcfVD  45890