Theorem in1 44542

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

Syntax hints:   → wi 4  (   wvd1 44540

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 44541

This theorem is referenced by:  vd12  44571  vd13  44572  gen11nv  44588  gen12  44589  exinst11  44597  e1a  44598  el1  44599  e223  44606  e111  44645  e1111  44646  el2122old  44690  el12  44697  el123  44735  un0.1  44750  trsspwALT  44789  sspwtr  44792  pwtrVD  44795  pwtrrVD  44796  snssiALTVD  44798  snsslVD  44800  snelpwrVD  44802  unipwrVD  44803  sstrALT2VD  44805  suctrALT2VD  44807  elex2VD  44809  elex22VD  44810  eqsbc2VD  44811  zfregs2VD  44812  tpid3gVD  44813  en3lplem1VD  44814  en3lplem2VD  44815  en3lpVD  44816  3ornot23VD  44818  orbi1rVD  44819  3orbi123VD  44821  sbc3orgVD  44822  19.21a3con13vVD  44823  exbirVD  44824  exbiriVD  44825  rspsbc2VD  44826  3impexpVD  44827  3impexpbicomVD  44828  sbcoreleleqVD  44830  tratrbVD  44832  al2imVD  44833  syl5impVD  44834  ssralv2VD  44837  ordelordALTVD  44838  equncomVD  44839  imbi12VD  44844  imbi13VD  44845  sbcim2gVD  44846  sbcbiVD  44847  trsbcVD  44848  truniALTVD  44849  trintALTVD  44851  undif3VD  44853  sbcssgVD  44854  csbingVD  44855  simplbi2comtVD  44859  onfrALTVD  44862  csbeq2gVD  44863  csbsngVD  44864  csbxpgVD  44865  csbresgVD  44866  csbrngVD  44867  csbima12gALTVD  44868  csbunigVD  44869  csbfv12gALTVD  44870  con5VD  44871  relopabVD  44872  19.41rgVD  44873  2pm13.193VD  44874  hbimpgVD  44875  hbalgVD  44876  hbexgVD  44877  ax6e2eqVD  44878  ax6e2ndVD  44879  ax6e2ndeqVD  44880  2sb5ndVD  44881  2uasbanhVD  44882  e2ebindVD  44883  sb5ALTVD  44884  vk15.4jVD  44885  notnotrALTVD  44886  con3ALTVD  44887  sspwimpVD  44890  sspwimpcfVD  44892  suctrALTcfVD  44894