Theorem in1 40912

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

Syntax hints:   → wi 4  (   wvd1 40910

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 209  df-vd1 40911

This theorem is referenced by:  vd12  40941  vd13  40942  gen11nv  40958  gen12  40959  exinst11  40967  e1a  40968  el1  40969  e223  40976  e111  41015  e1111  41016  el2122old  41060  el12  41067  el123  41105  un0.1  41120  trsspwALT  41159  sspwtr  41162  pwtrVD  41165  pwtrrVD  41166  snssiALTVD  41168  snsslVD  41170  snelpwrVD  41172  unipwrVD  41173  sstrALT2VD  41175  suctrALT2VD  41177  elex2VD  41179  elex22VD  41180  eqsbc3rVD  41181  zfregs2VD  41182  tpid3gVD  41183  en3lplem1VD  41184  en3lplem2VD  41185  en3lpVD  41186  3ornot23VD  41188  orbi1rVD  41189  3orbi123VD  41191  sbc3orgVD  41192  19.21a3con13vVD  41193  exbirVD  41194  exbiriVD  41195  rspsbc2VD  41196  3impexpVD  41197  3impexpbicomVD  41198  sbcoreleleqVD  41200  tratrbVD  41202  al2imVD  41203  syl5impVD  41204  ssralv2VD  41207  ordelordALTVD  41208  equncomVD  41209  imbi12VD  41214  imbi13VD  41215  sbcim2gVD  41216  sbcbiVD  41217  trsbcVD  41218  truniALTVD  41219  trintALTVD  41221  undif3VD  41223  sbcssgVD  41224  csbingVD  41225  simplbi2comtVD  41229  onfrALTVD  41232  csbeq2gVD  41233  csbsngVD  41234  csbxpgVD  41235  csbresgVD  41236  csbrngVD  41237  csbima12gALTVD  41238  csbunigVD  41239  csbfv12gALTVD  41240  con5VD  41241  relopabVD  41242  19.41rgVD  41243  2pm13.193VD  41244  hbimpgVD  41245  hbalgVD  41246  hbexgVD  41247  ax6e2eqVD  41248  ax6e2ndVD  41249  ax6e2ndeqVD  41250  2sb5ndVD  41251  2uasbanhVD  41252  e2ebindVD  41253  sb5ALTVD  41254  vk15.4jVD  41255  notnotrALTVD  41256  con3ALTVD  41257  sspwimpVD  41260  sspwimpcfVD  41262  suctrALTcfVD  41264