Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  in1 Structured version   Visualization version   GIF version

Theorem in1 39381
Description: Inference form of df-vd1 39380. 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
StepHypRef Expression
1 in1.1 . 2 (   𝜑   ▶   𝜓   )
2 df-vd1 39380 . 2 ((   𝜑   ▶   𝜓   ) ↔ (𝜑𝜓))
31, 2mpbi 221 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 39379
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 198  df-vd1 39380
This theorem is referenced by:  vd12  39419  vd13  39420  gen11nv  39436  gen12  39437  exinst11  39445  e1a  39446  el1  39447  e223  39454  e111  39493  e1111  39494  el2122old  39538  el12  39546  el123  39584  un0.1  39599  trsspwALT  39638  sspwtr  39641  pwtrVD  39644  pwtrrVD  39645  snssiALTVD  39647  snsslVD  39649  snelpwrVD  39651  unipwrVD  39652  sstrALT2VD  39654  suctrALT2VD  39656  elex2VD  39658  elex22VD  39659  eqsbc3rVD  39660  zfregs2VD  39661  tpid3gVD  39662  en3lplem1VD  39663  en3lplem2VD  39664  en3lpVD  39665  3ornot23VD  39667  orbi1rVD  39668  3orbi123VD  39670  sbc3orgVD  39671  19.21a3con13vVD  39672  exbirVD  39673  exbiriVD  39674  rspsbc2VD  39675  3impexpVD  39676  3impexpbicomVD  39677  sbcoreleleqVD  39679  tratrbVD  39681  al2imVD  39682  syl5impVD  39683  ssralv2VD  39686  ordelordALTVD  39687  equncomVD  39688  imbi12VD  39693  imbi13VD  39694  sbcim2gVD  39695  sbcbiVD  39696  trsbcVD  39697  truniALTVD  39698  trintALTVD  39700  undif3VD  39702  sbcssgVD  39703  csbingVD  39704  simplbi2comtVD  39708  onfrALTVD  39711  csbeq2gVD  39712  csbsngVD  39713  csbxpgVD  39714  csbresgVD  39715  csbrngVD  39716  csbima12gALTVD  39717  csbunigVD  39718  csbfv12gALTVD  39719  con5VD  39720  relopabVD  39721  19.41rgVD  39722  2pm13.193VD  39723  hbimpgVD  39724  hbalgVD  39725  hbexgVD  39726  ax6e2eqVD  39727  ax6e2ndVD  39728  ax6e2ndeqVD  39729  2sb5ndVD  39730  2uasbanhVD  39731  e2ebindVD  39732  sb5ALTVD  39733  vk15.4jVD  39734  notnotrALTVD  39735  con3ALTVD  39736  sspwimpVD  39739  sspwimpcfVD  39741  suctrALTcfVD  39743
  Copyright terms: Public domain W3C validator