NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  biimpi Structured version   Unicode version

Theorem biimpi 186
Description: Infer an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
biimpi.1
Assertion
Ref Expression
biimpi

Proof of Theorem biimpi
StepHypRef Expression
1 biimpi.1 . 2
2 bi1 178 . 2
31, 2ax-mp 8 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 176
This theorem is referenced by:  sylbi  187  sylib  188  biimpri  197  mpbi  199  syl5bi  208  syl6ib  217  syl7bi  221  syl8ib  222  bitri  240  pm2.53  362  simplbi  446  simprbi  450  sylanb  458  sylan2b  461  pm3.1  484  orbi2i  505  pm2.32  512  anc2l  538  pm3.37  562  dfbi  610  pm2.76  821  pm5.15  859  pm5.16  860  pm5.75  903  rnlem  931  simp1bi  970  simp2bi  971  simp3bi  972  syl3an1b  1218  syl3an2b  1219  syl3an3b  1220  nic-ax  1438  19.25  1603  sbbii  1653  spvw  1666  hbn1fw  1705  excomim  1742  stdpc5  1798  ax10-16  2190  exmoeu  2246  2mo  2282  eqeq1  2359  eleq2  2414  gencbvex  2901  moeq  3012  euind  3023  reuind  3039  eqsbc3r  3103  ssel  3267  unssd  3439  ssind  3479  n0moeu  3562  ss0  3581  uneqdifeq  3638  ssunsn2  3865  eqsn  3867  snex  4111  pwadjoin  4119  prprc2  4122  opkelimagekg  4271  iotabi  4348  uniabio  4349  iotaint  4352  dfiota4  4372  nnsucelrlem3  4425  nnsucelr  4427  nndisjeq  4428  ltfintri  4466  ssfin  4470  eqtfinrelk  4486  tfinsuc  4498  phi011lem1  4596  phidisjnn  4613  elrel  4850  dmxp  4935  resabs1  5007  resima2  5022  imasn  5033  coi2  5124  funcnv3  5191  funimass1  5205  funssxp  5271  f1o00  5357  fsn2  5474  oprabid  5589  eloprabga  5620  op1st2nd  5819  pw1fnf1o  5881  clos1induct  5902  peano4nc  6171  dflec2  6231  ce2le  6253  nchoice  6308
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator