Theorem in1 45394

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

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

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 45393

This theorem is used by:  vd12  45423  vd13  45424  gen11nv  45440  gen12  45441  exinst11  45449  e1a  45450  el1  45451  e223  45458  e111  45497  e1111  45498  el2122old  45541  el12  45548  el123  45586  un0.1  45601  trsspwALT  45640  sspwtr  45643  pwtrVD  45646  pwtrrVD  45647  snssiALTVD  45649  snsslVD  45651  snelpwrVD  45653  unipwrVD  45654  sstrALT2VD  45656  suctrALT2VD  45658  elex2VD  45660  elex22VD  45661  eqsbc2VD  45662  zfregs2VD  45663  tpid3gVD  45664  en3lplem1VD  45665  en3lplem2VD  45666  en3lpVD  45667  3ornot23VD  45669  orbi1rVD  45670  3orbi123VD  45672  sbc3orgVD  45673  19.21a3con13vVD  45674  exbirVD  45675  exbiriVD  45676  rspsbc2VD  45677  3impexpVD  45678  3impexpbicomVD  45679  sbcoreleleqVD  45681  tratrbVD  45683  al2imVD  45684  syl5impVD  45685  ssralv2VD  45688  ordelordALTVD  45689  equncomVD  45690  imbi12VD  45695  imbi13VD  45696  sbcim2gVD  45697  sbcbiVD  45698  trsbcVD  45699  truniALTVD  45700  trintALTVD  45702  undif3VD  45704  sbcssgVD  45705  csbingVD  45706  simplbi2comtVD  45710  onfrALTVD  45713  csbeq2gVD  45714  csbsngVD  45715  csbxpgVD  45716  csbresgVD  45717  csbrngVD  45718  csbima12gALTVD  45719  csbunigVD  45720  csbfv12gALTVD  45721  con5VD  45722  relopabVD  45723  19.41rgVD  45724  2pm13.193VD  45725  hbimpgVD  45726  hbalgVD  45727  hbexgVD  45728  ax6e2eqVD  45729  ax6e2ndVD  45730  ax6e2ndeqVD  45731  2sb5ndVD  45732  2uasbanhVD  45733  e2ebindVD  45734  sb5ALTVD  45735  vk15.4jVD  45736  notnotrALTVD  45737  con3ALTVD  45738  sspwimpVD  45741  sspwimpcfVD  45743  suctrALTcfVD  45745