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  4255  uniex2  4581  dcextest  4728  tfi  4729  peano5  4745  opelxpi  4806  ndmima  5164  iotass  5355  dffo2  5619  dff1o2  5644  resdif  5661  f1o00  5676  ressnop0  5896  fsnunfv  5916  ovid  6205  ovidig  6206  f1stres  6393  f2ndres  6394  rdgon  6657  elixpsn  7017  modom  7108  diffisn  7197  diffifi  7198  unsnfi  7226  snexxph  7267  ordiso2  7375  omp1eomlem  7434  ltexnqq  7775  enq0sym  7799  prarloclem5  7867  nqprloc  7912  nqprl  7918  nqpru  7919  pitonn  8215  axcnre  8248  peano5nnnn  8259  axcaucvglemres  8266  le2tri3i  8434  muldivdirap  9037  peano5nni  9307  0nn0  9578  uzind4  9988  elfz4  10421  eluzfz  10423  ssfzo12bi  10643  ioom  10695  ser0  10970  exp3vallem  10977  hashinfuni  11216  hashxp  11267  wrdsymb1  11341  ccatfv0  11371  lswccats1fst  11412  ccatswrd  11442  ccatpfx  11473  nn0abscl  11851  fimaxre2  11993  iserle  12108  climserle  12111  summodclem2a  12148  fsumcl2lem  12165  fsumadd  12173  sumsnf  12176  isumclim3  12190  isumadd  12198  sumsplitdc  12199  fsummulc2  12215  cvgcmpub  12243  isumshft  12257  isumlessdc  12263  trireciplem  12267  geolim  12278  geo2lim  12283  cvgratz  12299  mertenslem2  12303  mertensabs  12304  prodmodclem3  12342  prodmodclem2a  12343  zproddc  12346  fprodmul  12358  prodsnf  12359  ef0lem  12427  efcvgfsum  12434  ege2le3  12438  efcj  12440  efgt1p2  12462  ndvdsadd  12698  gcdsupex  12734  gcdsupcl  12735  ialgrlemconst  12821  divgcdcoprmex  12880  1idssfct  12893  odzdvds  13024  nninfdclemp1  13341  divsfval  13649  xpsfrnel2  13667  xpsff1o  13670  mulgnndir  13954  opprdrng  14620  rmodislmodlem  14687  rmodislmod  14688  isassa  15002  tgcl  15165  txcnp  15372  ivthdich  15754  plyval  15833  logfac  15995  lgsval2lem  16129  lgsdir  16154  lgsdilem2  16155  lgsdi  16156  lgsne0  16157  lgsmodeq  16164  lgsmulsqcoprm  16165  2lgs  16223  bj-charfunbi  16837  bj-sucexg  16948  bj-indind  16958  bj-2inf  16964  findset  16971  trilpolemisumle  17087  nconstwlpolem0  17113