Theorem in1 40903

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

Syntax hints:   → wi 4  (   wvd1 40901

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 40902

This theorem is referenced by:  vd12  40932  vd13  40933  gen11nv  40949  gen12  40950  exinst11  40958  e1a  40959  el1  40960  e223  40967  e111  41006  e1111  41007  el2122old  41051  el12  41058  el123  41096  un0.1  41111  trsspwALT  41150  sspwtr  41153  pwtrVD  41156  pwtrrVD  41157  snssiALTVD  41159  snsslVD  41161  snelpwrVD  41163  unipwrVD  41164  sstrALT2VD  41166  suctrALT2VD  41168  elex2VD  41170  elex22VD  41171  eqsbc3rVD  41172  zfregs2VD  41173  tpid3gVD  41174  en3lplem1VD  41175  en3lplem2VD  41176  en3lpVD  41177  3ornot23VD  41179  orbi1rVD  41180  3orbi123VD  41182  sbc3orgVD  41183  19.21a3con13vVD  41184  exbirVD  41185  exbiriVD  41186  rspsbc2VD  41187  3impexpVD  41188  3impexpbicomVD  41189  sbcoreleleqVD  41191  tratrbVD  41193  al2imVD  41194  syl5impVD  41195  ssralv2VD  41198  ordelordALTVD  41199  equncomVD  41200  imbi12VD  41205  imbi13VD  41206  sbcim2gVD  41207  sbcbiVD  41208  trsbcVD  41209  truniALTVD  41210  trintALTVD  41212  undif3VD  41214  sbcssgVD  41215  csbingVD  41216  simplbi2comtVD  41220  onfrALTVD  41223  csbeq2gVD  41224  csbsngVD  41225  csbxpgVD  41226  csbresgVD  41227  csbrngVD  41228  csbima12gALTVD  41229  csbunigVD  41230  csbfv12gALTVD  41231  con5VD  41232  relopabVD  41233  19.41rgVD  41234  2pm13.193VD  41235  hbimpgVD  41236  hbalgVD  41237  hbexgVD  41238  ax6e2eqVD  41239  ax6e2ndVD  41240  ax6e2ndeqVD  41241  2sb5ndVD  41242  2uasbanhVD  41243  e2ebindVD  41244  sb5ALTVD  41245  vk15.4jVD  41246  notnotrALTVD  41247  con3ALTVD  41248  sspwimpVD  41251  sspwimpcfVD  41253  suctrALTcfVD  41255