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

Theorem biimpri 132
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 131 . 2  |-  ( ps  <->  ph )
32biimpi 119 1  |-  ( ps 
->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  sylibr  133  sylbir  134  sylbbr  135  sylbb1  136  sylbb2  137  mpbir  145  syl5bir  152  syl6ibr  161  bitri  183  sylanbr  283  sylan2br  286  simplbi2  382  sylanblrc  412  mtbi  644  pm3.44  689  orbi2i  736  pm2.31  742  dcor  904  rnlem  945  syl3an1br  1240  syl3an2br  1241  syl3an3br  1242  xorbin  1347  3impexpbicom  1399  equveli  1717  sbbii  1723  dveeq2or  1772  exmoeudc  2040  eueq2dc  2830  ralun  3228  undif3ss  3307  ssunieq  3739  a9evsep  4020  dcextest  4465  tfi  4466  peano5  4482  opelxpi  4541  ndmima  4886  iotass  5075  dffo2  5319  dff1o2  5340  resdif  5357  f1o00  5370  ressnop0  5569  fsnunfv  5589  ovid  5855  ovidig  5856  f1stres  6025  f2ndres  6026  rdgon  6251  elixpsn  6597  diffisn  6755  diffifi  6756  unsnfi  6775  snexxph  6806  ordiso2  6888  omp1eomlem  6947  ltexnqq  7184  enq0sym  7208  prarloclem5  7276  nqprloc  7321  nqprl  7327  nqpru  7328  pitonn  7624  axcnre  7657  peano5nnnn  7668  axcaucvglemres  7675  le2tri3i  7840  muldivdirap  8435  peano5nni  8691  0nn0  8960  uzind4  9351  elfz4  9767  eluzfz  9769  ssfzo12bi  9970  ioom  10006  ser0  10255  exp3vallem  10262  hashinfuni  10491  hashxp  10540  nn0abscl  10825  fimaxre2  10966  iserle  11079  climserle  11082  summodclem2a  11118  fsumcl2lem  11135  fsumadd  11143  sumsnf  11146  isumclim3  11160  isumadd  11168  sumsplitdc  11169  fsummulc2  11185  cvgcmpub  11213  isumshft  11227  isumlessdc  11233  trireciplem  11237  geolim  11248  geo2lim  11253  cvgratz  11269  mertenslem2  11273  mertensabs  11274  ef0lem  11293  efcvgfsum  11300  ege2le3  11304  efcj  11306  efgt1p2  11328  ndvdsadd  11555  gcdsupex  11573  gcdsupcl  11574  ialgrlemconst  11651  divgcdcoprmex  11710  1idssfct  11723  tgcl  12160  txcnp  12367  bj-sucexg  13047  bj-indind  13057  bj-2inf  13063  findset  13070  trilpolemisumle  13158
  Copyright terms: Public domain W3C validator