Theorem in1 37808

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

Syntax hints:   → wi 4  (   wvd1 37806

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 196  df-vd1 37807

This theorem is referenced by:  vd12  37846  vd13  37847  gen11nv  37863  gen12  37864  exinst11  37872  e1a  37873  el1  37874  e223  37881  e111  37920  e1111  37921  el2122old  37965  el12  37974  el123  38012  un0.1  38027  trsspwALT  38067  sspwtr  38070  pwtrVD  38081  pwtrrVD  38082  snssiALTVD  38084  snsslVD  38086  snelpwrVD  38088  unipwrVD  38089  sstrALT2VD  38091  suctrALT2VD  38093  elex2VD  38095  elex22VD  38096  eqsbc3rVD  38097  zfregs2VD  38098  tpid3gVD  38099  en3lplem1VD  38100  en3lplem2VD  38101  en3lpVD  38102  3ornot23VD  38104  orbi1rVD  38105  3orbi123VD  38107  sbc3orgVD  38108  19.21a3con13vVD  38109  exbirVD  38110  exbiriVD  38111  rspsbc2VD  38112  3impexpVD  38113  3impexpbicomVD  38114  sbcoreleleqVD  38117  tratrbVD  38119  al2imVD  38120  syl5impVD  38121  ssralv2VD  38124  ordelordALTVD  38125  equncomVD  38126  imbi12VD  38131  imbi13VD  38132  sbcim2gVD  38133  sbcbiVD  38134  trsbcVD  38135  truniALTVD  38136  trintALTVD  38138  undif3VD  38140  sbcssgVD  38141  csbingVD  38142  simplbi2comtVD  38146  onfrALTVD  38149  csbeq2gVD  38150  csbsngVD  38151  csbxpgVD  38152  csbresgVD  38153  csbrngVD  38154  csbima12gALTVD  38155  csbunigVD  38156  csbfv12gALTVD  38157  con5VD  38158  relopabVD  38159  19.41rgVD  38160  2pm13.193VD  38161  hbimpgVD  38162  hbalgVD  38163  hbexgVD  38164  ax6e2eqVD  38165  ax6e2ndVD  38166  ax6e2ndeqVD  38167  2sb5ndVD  38168  2uasbanhVD  38169  e2ebindVD  38170  sb5ALTVD  38171  vk15.4jVD  38172  notnotrALTVD  38173  con3ALTVD  38174  sspwimpVD  38177  sspwimpcfVD  38179  suctrALTcfVD  38181