ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimpri Unicode version

Theorem biimpri 131
Description: Infer a converse implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Sep-2013.)
Hypothesis
Ref Expression
biimpri.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
biimpri  |-  ( ps 
->  ph )

Proof of Theorem biimpri
StepHypRef Expression
1 biimpri.1 . . 3  |-  ( ph  <->  ps )
21bicomi 130 . 2  |-  ( ps  <->  ph )
32biimpi 118 1  |-  ( ps 
->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  sylibr  132  sylbir  133  sylbbr  134  sylbb1  135  sylbb2  136  mpbir  144  syl5bir  151  syl6ibr  160  bitri  182  sylanbr  279  sylan2br  282  simplbi2  377  sylanblrc  407  mtbi  630  pm3.44  670  orbi2i  714  pm2.31  720  dcor  881  rnlem  922  syl3an1br  1213  syl3an2br  1214  syl3an3br  1215  xorbin  1320  3impexpbicom  1372  equveli  1689  sbbii  1695  dveeq2or  1744  exmoeudc  2011  eueq2dc  2786  ralun  3180  undif3ss  3258  ssunieq  3681  a9evsep  3953  dcextest  4386  tfi  4387  peano5  4403  opelxpi  4459  ndmima  4796  iotass  4984  dffo2  5221  dff1o2  5242  resdif  5259  f1o00  5272  ressnop0  5462  fsnunfv  5481  ovid  5743  ovidig  5744  f1stres  5912  f2ndres  5913  rdgon  6133  diffisn  6589  diffifi  6590  unsnfi  6609  snexxph  6638  ordiso2  6707  ltexnqq  6946  enq0sym  6970  prarloclem5  7038  nqprloc  7083  nqprl  7089  nqpru  7090  pitonn  7364  axcnre  7395  peano5nnnn  7406  axcaucvglemres  7413  le2tri3i  7572  muldivdirap  8148  peano5nni  8397  0nn0  8658  uzind4  9045  elfz4  9402  eluzfz  9404  ssfzo12bi  9601  ioom  9637  iser0  9912  ser0  9914  exp3vallem  9921  hashinfuni  10150  hashxp  10199  nn0abscl  10483  fimaxre2  10622  iserle  10695  climserle  10698  isummolem2a  10735  fsum3  10743  fsumcl2lem  10755  fsumadd  10763  sumsnf  10766  isumclim3  10780  isummulc2  10783  isumadd  10788  sumsplitdc  10789  fsummulc2  10805  cvgcmpub  10832  isumshft  10846  trireciplem  10855  geolim  10866  geo2lim  10871  cvgratz  10887  ndvdsadd  11024  gcdsupex  11042  gcdsupcl  11043  ialgrlemconst  11118  divgcdcoprmex  11177  1idssfct  11190  bj-sucexg  11470  bj-indind  11484  bj-2inf  11490  findset  11497
  Copyright terms: Public domain W3C validator