Theorem in1 45338

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

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

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 45337

This theorem is used by:  vd12  45367  vd13  45368  gen11nv  45384  gen12  45385  exinst11  45393  e1a  45394  el1  45395  e223  45402  e111  45441  e1111  45442  el2122old  45485  el12  45492  el123  45530  un0.1  45545  trsspwALT  45584  sspwtr  45587  pwtrVD  45590  pwtrrVD  45591  snssiALTVD  45593  snsslVD  45595  snelpwrVD  45597  unipwrVD  45598  sstrALT2VD  45600  suctrALT2VD  45602  elex2VD  45604  elex22VD  45605  eqsbc2VD  45606  zfregs2VD  45607  tpid3gVD  45608  en3lplem1VD  45609  en3lplem2VD  45610  en3lpVD  45611  3ornot23VD  45613  orbi1rVD  45614  3orbi123VD  45616  sbc3orgVD  45617  19.21a3con13vVD  45618  exbirVD  45619  exbiriVD  45620  rspsbc2VD  45621  3impexpVD  45622  3impexpbicomVD  45623  sbcoreleleqVD  45625  tratrbVD  45627  al2imVD  45628  syl5impVD  45629  ssralv2VD  45632  ordelordALTVD  45633  equncomVD  45634  imbi12VD  45639  imbi13VD  45640  sbcim2gVD  45641  sbcbiVD  45642  trsbcVD  45643  truniALTVD  45644  trintALTVD  45646  undif3VD  45648  sbcssgVD  45649  csbingVD  45650  simplbi2comtVD  45654  onfrALTVD  45657  csbeq2gVD  45658  csbsngVD  45659  csbxpgVD  45660  csbresgVD  45661  csbrngVD  45662  csbima12gALTVD  45663  csbunigVD  45664  csbfv12gALTVD  45665  con5VD  45666  relopabVD  45667  19.41rgVD  45668  2pm13.193VD  45669  hbimpgVD  45670  hbalgVD  45671  hbexgVD  45672  ax6e2eqVD  45673  ax6e2ndVD  45674  ax6e2ndeqVD  45675  2sb5ndVD  45676  2uasbanhVD  45677  e2ebindVD  45678  sb5ALTVD  45679  vk15.4jVD  45680  notnotrALTVD  45681  con3ALTVD  45682  sspwimpVD  45685  sspwimpcfVD  45687  suctrALTcfVD  45689