Theorem in1 44534

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

Syntax hints:   → wi 4  (   wvd1 44532

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 44533

This theorem is referenced by:  vd12  44563  vd13  44564  gen11nv  44580  gen12  44581  exinst11  44589  e1a  44590  el1  44591  e223  44598  e111  44637  e1111  44638  el2122old  44681  el12  44688  el123  44726  un0.1  44741  trsspwALT  44780  sspwtr  44783  pwtrVD  44786  pwtrrVD  44787  snssiALTVD  44789  snsslVD  44791  snelpwrVD  44793  unipwrVD  44794  sstrALT2VD  44796  suctrALT2VD  44798  elex2VD  44800  elex22VD  44801  eqsbc2VD  44802  zfregs2VD  44803  tpid3gVD  44804  en3lplem1VD  44805  en3lplem2VD  44806  en3lpVD  44807  3ornot23VD  44809  orbi1rVD  44810  3orbi123VD  44812  sbc3orgVD  44813  19.21a3con13vVD  44814  exbirVD  44815  exbiriVD  44816  rspsbc2VD  44817  3impexpVD  44818  3impexpbicomVD  44819  sbcoreleleqVD  44821  tratrbVD  44823  al2imVD  44824  syl5impVD  44825  ssralv2VD  44828  ordelordALTVD  44829  equncomVD  44830  imbi12VD  44835  imbi13VD  44836  sbcim2gVD  44837  sbcbiVD  44838  trsbcVD  44839  truniALTVD  44840  trintALTVD  44842  undif3VD  44844  sbcssgVD  44845  csbingVD  44846  simplbi2comtVD  44850  onfrALTVD  44853  csbeq2gVD  44854  csbsngVD  44855  csbxpgVD  44856  csbresgVD  44857  csbrngVD  44858  csbima12gALTVD  44859  csbunigVD  44860  csbfv12gALTVD  44861  con5VD  44862  relopabVD  44863  19.41rgVD  44864  2pm13.193VD  44865  hbimpgVD  44866  hbalgVD  44867  hbexgVD  44868  ax6e2eqVD  44869  ax6e2ndVD  44870  ax6e2ndeqVD  44871  2sb5ndVD  44872  2uasbanhVD  44873  e2ebindVD  44874  sb5ALTVD  44875  vk15.4jVD  44876  notnotrALTVD  44877  con3ALTVD  44878  sspwimpVD  44881  sspwimpcfVD  44883  suctrALTcfVD  44885