Theorem in1 45814

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

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

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 45813

This theorem is used by:  vd12  45843  vd13  45844  gen11nv  45860  gen12  45861  exinst11  45869  e1a  45870  el1  45871  e223  45878  e111  45917  e1111  45918  el2122old  45961  el12  45968  el123  46006  un0.1  46021  trsspwALT  46060  sspwtr  46063  pwtrVD  46066  pwtrrVD  46067  snssiALTVD  46069  snsslVD  46071  snelpwrVD  46073  unipwrVD  46074  sstrALT2VD  46076  suctrALT2VD  46078  elex2VD  46080  elex22VD  46081  eqsbc2VD  46082  zfregs2VD  46083  tpid3gVD  46084  en3lplem1VD  46085  en3lplem2VD  46086  en3lpVD  46087  3ornot23VD  46089  orbi1rVD  46090  3orbi123VD  46092  sbc3orgVD  46093  19.21a3con13vVD  46094  exbirVD  46095  exbiriVD  46096  rspsbc2VD  46097  3impexpVD  46098  3impexpbicomVD  46099  sbcoreleleqVD  46101  tratrbVD  46103  al2imVD  46104  syl5impVD  46105  ssralv2VD  46108  ordelordALTVD  46109  equncomVD  46110  imbi12VD  46115  imbi13VD  46116  sbcim2gVD  46117  sbcbiVD  46118  trsbcVD  46119  truniALTVD  46120  trintALTVD  46122  undif3VD  46124  sbcssgVD  46125  csbingVD  46126  simplbi2comtVD  46130  onfrALTVD  46133  csbeq2gVD  46134  csbsngVD  46135  csbxpgVD  46136  csbresgVD  46137  csbrngVD  46138  csbima12gALTVD  46139  csbunigVD  46140  csbfv12gALTVD  46141  con5VD  46142  relopabVD  46143  19.41rgVD  46144  2pm13.193VD  46145  hbimpgVD  46146  hbalgVD  46147  hbexgVD  46148  ax6e2eqVD  46149  ax6e2ndVD  46150  ax6e2ndeqVD  46151  2sb5ndVD  46152  2uasbanhVD  46153  e2ebindVD  46154  sb5ALTVD  46155  vk15.4jVD  46156  notnotrALTVD  46157  con3ALTVD  46158  sspwimpVD  46161  sspwimpcfVD  46163  suctrALTcfVD  46165