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

Step	Hyp	Ref	Expression
1		biimpri.1	. . 3 |- ( ph <-> ps )
2	1	bicomi 132	. 2 |- ( ps <-> ph )
3	2	biimpi 120	1 |- ( ps -> ph )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylibr  134  sylbir  135  sylbbr  136  sylbb1  137  sylbb2  138  mpbir  146  biimtrrid  153  imbitrrdi  162  bitri  184  sylanbr  285  sylan2br  288  simplbi2  385  biranri  388  bilanri  389  sylanblrc  420  mtbi  681  pm3.44  727  orbi2i  774  pm2.31  780  dcor  948  rnlem  989  syl3an1br  1317  syl3an2br  1318  syl3an3br  1319  xorbin  1433  3impexpbicom  1488  equveli  1812  sbbii  1818  dveeq2or  1869  exmoeudc  2150  nfabdw  2411  eueq2dc  2999  ralun  3411  undif3ss  3492  ssunieq  3968  a9evsep  4257  uniex2  4583  dcextest  4730  tfi  4731  peano5  4747  opelxpi  4808  ndmima  5167  iotass  5358  dffo2  5622  dff1o2  5647  resdif  5664  f1o00  5679  ressnop0  5899  fsnunfv  5919  ovid  6208  ovidig  6209  f1stres  6397  f2ndres  6398  rdgon  6661  elixpsn  7021  modom  7112  diffisn  7201  diffifi  7202  unsnfi  7230  snexxph  7272  ordiso2  7381  omp1eomlem  7440  ltexnqq  7781  enq0sym  7805  prarloclem5  7873  nqprloc  7918  nqprl  7924  nqpru  7925  pitonn  8221  axcnre  8254  peano5nnnn  8265  axcaucvglemres  8272  le2tri3i  8441  muldivdirap  9045  peano5nni  9316  0nn0  9589  uzind4  10004  elfz4  10438  eluzfz  10440  ssfzo12bi  10660  ioom  10712  ser0  10991  exp3vallem  10998  hashinfuni  11238  hashxp  11289  wrdsymb1  11363  ccatfv0  11393  lswccats1fst  11434  ccatswrd  11464  ccatpfx  11495  nn0abscl  11874  fimaxre2  12016  iserle  12133  climserle  12136  summodclem2a  12173  fsumcl2lem  12190  fsumadd  12198  sumsnf  12201  isumclim3  12215  isumadd  12223  sumsplitdc  12224  fsummulc2  12240  cvgcmpub  12268  isumshft  12282  isumlessdc  12288  trireciplem  12292  geolim  12303  geo2lim  12308  cvgratz  12324  mertenslem2  12328  mertensabs  12329  prodmodclem3  12367  prodmodclem2a  12368  zproddc  12371  fprodmul  12383  prodsnf  12384  ef0lem  12452  efcvgfsum  12459  ege2le3  12463  efcj  12465  efgt1p2  12487  ndvdsadd  12723  gcdsupex  12759  gcdsupcl  12760  ialgrlemconst  12846  divgcdcoprmex  12905  1idssfct  12918  odzdvds  13053  nninfdclemp1  13399  divsfval  13708  xpsfrnel2  13726  xpsff1o  13729  mulgnndir  14013  gsummptfidmsplit  14254  gsumresfi  14263  opprdrng  14729  rmodislmodlem  14796  rmodislmod  14797  isassa  15111  tgcl  15290  txcnp  15497  ivthdich  15879  plyval  15958  logfac  16126  lgsval2lem  16334  lgsdir  16359  lgsdilem2  16360  lgsdi  16361  lgsne0  16362  lgsmodeq  16369  lgsmulsqcoprm  16370  2lgs  16428  bj-charfunbi  17042  bj-sucexg  17153  bj-indind  17163  bj-2inf  17169  findset  17176  trilpolemisumle  17294  nconstwlpolem0  17320