Theorem in1 16481

Description: Inference form of df-vd1 16480. Virtual deduction introduction rule of converting the virtual hypothesis of a 1-virtual hypothesis virtual deduction into an antecedent.

Hypothesis

Ref	Expression
in1.1	|- . ph   ⊢   ps .

Assertion

Ref	Expression
in1	|- (ph -> ps)

Proof of Theorem in1

Step	Hyp	Ref	Expression
1		in1.1	. 2 |- . ph   ⊢   ps .
2		df-vd1 16480	. 2 |- ( . ph   ⊢   ps . <-> (ph -> ps))
3	1, 2	mpbi 206	1 |- (ph -> ps)

Syntax hints:   -> wi 3   . vd1 16479

This theorem is referenced by:  vd12 16501  vd13 16502  gen11nv 16512  gen12 16513  e1_ 16518  e223 16525  e111 16564  e1111 16565  trsspwALT 16640  sspwtr 16643  pwtrVD 16646  pwtrrVD 16648  snssiALTVD 16650  snsslVD 16652  snelpwrVD 16654  unipwrVD 16656  sstrALT2VD 16658  suctrALT2VD 16660  elex2VD 16662  elex22VD 16663  eqsbc3rVD 16664  zfregs2VD 16665  tpid3gVD 16666  en3lplem1VD 16667  en3lplem2VD 16668  en3lpVD 16669  3ornot23VD 16671  orbi1rVD 16672  bitr3VD 16673  3orbi123VD 16674  sbc3orgVD 16675  19.21a3con13vVD 16676  exbirVD 16677  exbiriVD 16678  ra4sbc2VD 16679  3impexpVD 16680  3impexpbicomVD 16681  sbcoreleleqVD 16683  tratrbVD 16685  3ax5VD 16686  syl5impVD 16687  ssralv2VD 16690  ordelordaxrVD 16691  equncomVD 16692  imbi12VD 16697  imbi13VD 16698  sbcim2gVD 16699  sbcbiVD 16700  trsbcVD 16701  truniALTVD 16702  trintALTVD 16704  undif3VD 16706

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-vd1 16480

Copyright terms: Public domain