Theorem in1 45280

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

Syntax hints:   → wi 4  (   wvd1 45278

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 210  df-vd1 45279

This theorem is referenced by:  vd12  45309  vd13  45310  gen11nv  45326  gen12  45327  exinst11  45335  e1a  45336  el1  45337  e223  45344  e111  45383  e1111  45384  el2122old  45427  el12  45434  el123  45472  un0.1  45487  trsspwALT  45526  sspwtr  45529  pwtrVD  45532  pwtrrVD  45533  snssiALTVD  45535  snsslVD  45537  snelpwrVD  45539  unipwrVD  45540  sstrALT2VD  45542  suctrALT2VD  45544  elex2VD  45546  elex22VD  45547  eqsbc2VD  45548  zfregs2VD  45549  tpid3gVD  45550  en3lplem1VD  45551  en3lplem2VD  45552  en3lpVD  45553  3ornot23VD  45555  orbi1rVD  45556  3orbi123VD  45558  sbc3orgVD  45559  19.21a3con13vVD  45560  exbirVD  45561  exbiriVD  45562  rspsbc2VD  45563  3impexpVD  45564  3impexpbicomVD  45565  sbcoreleleqVD  45567  tratrbVD  45569  al2imVD  45570  syl5impVD  45571  ssralv2VD  45574  ordelordALTVD  45575  equncomVD  45576  imbi12VD  45581  imbi13VD  45582  sbcim2gVD  45583  sbcbiVD  45584  trsbcVD  45585  truniALTVD  45586  trintALTVD  45588  undif3VD  45590  sbcssgVD  45591  csbingVD  45592  simplbi2comtVD  45596  onfrALTVD  45599  csbeq2gVD  45600  csbsngVD  45601  csbxpgVD  45602  csbresgVD  45603  csbrngVD  45604  csbima12gALTVD  45605  csbunigVD  45606  csbfv12gALTVD  45607  con5VD  45608  relopabVD  45609  19.41rgVD  45610  2pm13.193VD  45611  hbimpgVD  45612  hbalgVD  45613  hbexgVD  45614  ax6e2eqVD  45615  ax6e2ndVD  45616  ax6e2ndeqVD  45617  2sb5ndVD  45618  2uasbanhVD  45619  e2ebindVD  45620  sb5ALTVD  45621  vk15.4jVD  45622  notnotrALTVD  45623  con3ALTVD  45624  sspwimpVD  45627  sspwimpcfVD  45629  suctrALTcfVD  45631