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

Theorem biimpri 133
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 132 . 2  |-  ( ps  <->  ph )
32biimpi 120 1  |-  ( ps 
->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  sylibr  134  sylbir  135  sylbbr  136  sylbb1  137  sylbb2  138  mpbir  146  biimtrrid  153  syl6ibr  162  bitri  184  sylanbr  285  sylan2br  288  simplbi2  385  sylanblrc  416  mtbi  670  pm3.44  715  orbi2i  762  pm2.31  768  dcor  935  rnlem  976  syl3an1br  1277  syl3an2br  1278  syl3an3br  1279  xorbin  1384  3impexpbicom  1438  equveli  1759  sbbii  1765  dveeq2or  1816  exmoeudc  2089  nfabdw  2338  eueq2dc  2910  ralun  3317  undif3ss  3396  ssunieq  3840  a9evsep  4122  dcextest  4576  tfi  4577  peano5  4593  opelxpi  4654  ndmima  5000  iotass  5190  dffo2  5437  dff1o2  5461  resdif  5478  f1o00  5491  ressnop0  5692  fsnunfv  5712  ovid  5984  ovidig  5985  f1stres  6153  f2ndres  6154  rdgon  6380  elixpsn  6728  diffisn  6886  diffifi  6887  unsnfi  6911  snexxph  6942  ordiso2  7027  omp1eomlem  7086  ltexnqq  7385  enq0sym  7409  prarloclem5  7477  nqprloc  7522  nqprl  7528  nqpru  7529  pitonn  7825  axcnre  7858  peano5nnnn  7869  axcaucvglemres  7876  le2tri3i  8043  muldivdirap  8640  peano5nni  8898  0nn0  9167  uzind4  9564  elfz4  9991  eluzfz  9993  ssfzo12bi  10198  ioom  10234  ser0  10487  exp3vallem  10494  hashinfuni  10728  hashxp  10777  nn0abscl  11065  fimaxre2  11206  iserle  11321  climserle  11324  summodclem2a  11360  fsumcl2lem  11377  fsumadd  11385  sumsnf  11388  isumclim3  11402  isumadd  11410  sumsplitdc  11411  fsummulc2  11427  cvgcmpub  11455  isumshft  11469  isumlessdc  11475  trireciplem  11479  geolim  11490  geo2lim  11495  cvgratz  11511  mertenslem2  11515  mertensabs  11516  prodmodclem3  11554  prodmodclem2a  11555  zproddc  11558  fprodmul  11570  prodsnf  11571  ef0lem  11639  efcvgfsum  11646  ege2le3  11650  efcj  11652  efgt1p2  11674  ndvdsadd  11906  gcdsupex  11928  gcdsupcl  11929  ialgrlemconst  12013  divgcdcoprmex  12072  1idssfct  12085  odzdvds  12215  nninfdclemp1  12421  mulgnndir  12887  tgcl  13197  txcnp  13404  lgsval2lem  14044  lgsdir  14069  lgsdilem2  14070  lgsdi  14071  lgsne0  14072  lgsmodeq  14079  lgsmulsqcoprm  14080  bj-charfunbi  14185  bj-sucexg  14296  bj-indind  14306  bj-2inf  14312  findset  14319  trilpolemisumle  14409  nconstwlpolem0  14433
  Copyright terms: Public domain W3C validator