Theorem impbi 157

Description: Infer an equivalence from an implication and its converse.

Hypotheses

Ref	Expression
impbi.1	|- (ph -> ps)
impbi.2	|- (ps -> ph)

Assertion

Ref	Expression
impbi	|- (ph <-> ps)

Proof of Theorem impbi

Step	Hyp	Ref	Expression
1		impbi.1	. 2 |- (ph -> ps)
2		impbi.2	. 2 |- (ps -> ph)
3		bi3 150	. 2 |- ((ph -> ps) -> ((ps -> ph) -> (ph <-> ps)))
4	1, 2, 3	mp2 43	1 |- (ph <-> ps)

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  dfbi1 158  bi2.04 160  pm4.13 161  pm4.8 162  pm4.81 163  pm4.1 164  bi2.03 165  bi2.15 166  pm5.4 167  imdi 168  pm5.41 169  pm4.2 170  bicomi 172  bitr 173  imbi2i 185  imbi1i 186  negbii 187  a1bi 197  con1bii 220  dfor2 229  oridm 243  anclb 329  ancrb 330  pm4.45im 332  pm4.44 345  pm5.63 346  impexp 347  jaob 422  pm4.43 431  anidm 432  ancom 435  imdistan 442  pm5.3 446  pm5.61 447  abai 479  anbi2i 480  anabs1 492  anabs7 494  orabs 581  pm5.74 583  ordi 596  pm4.71 635  pm4.72 641  oibabs 654  pm5.18 660  mt2bi 713  2th 718  bianfi 737  pm4.82 739  orbidi 743  consensus 767  19.3 1031  alcom 1032  19.9 1036  excom 1046  19.21 1056  19.23 1063  19.26 1067  equcom 1129  equsal 1151  sbbii 1174  sbf 1186  sb6x 1188  equs45f 1200  sb6f 1201  dfsb2 1225  sbn 1231  sbim 1234  sb5rf 1259  sb6rf 1260  sb8 1261  sb9 1264  equvin 1275  mo 1393  eu2 1396  mo2 1400  exmoeu 1413  2mo 1447  2eu6 1454  ralcom3 1777  rabab 1822  ceqsex 1834  gencbvex2 1839  euxfr2 1926  reu3 1931  reu6 1932  sspss 2145  ssin 2232  unineq 2255  uneqin 2256  difrab 2273  un00 2306  vss 2307  ralf0 2359  elpr2 2425  snidb 2434  disjsn 2441  pwpw0 2469  prss 2471  sssn 2473  sspr 2475  tpss 2476  preq12b 2483  preqsn 2486  pwsnALT 2501  iununi 2616  intex 2729  intnex 2730  iin0 2740  sspwb 2755  sspwuni 2758  opth 2787  opprc1b 2796  opprc3 2797  opthwiener 2807  ssopab2 2822  pwssun 2827  pwundif 2828  unexb 2873  ralxfr 2899  reuxfr2 2903  uniexb 2907  iunpw 2914  dfwe2 2935  elon2 2959  ordeleqon 2990  onintrab 3013  unon 3088  onuninsuc 3108  ordzsl 3116  dflim3 3118  ralxp 3218  opthprc 3221  relop 3275  issetid 3280  xpid11 3335  iss 3397  cotr 3436  cnvsym 3437  asymref2 3440  xpnz 3466  ssrnres 3481  dfrel2 3485  unixp0 3518  dffun7 3540  fn0 3605  fnopabg 3615  fnf 3628  funssxp 3638  f00 3657  dffo2 3675  f1o2 3693  ffoss 3711  f1o00 3714  fo00 3715  fv3 3733  fnopabfv 3758  dff4 3816  dff2 3817  dffo4 3820  dffo5 3821  exfo 3822  fopab2 3823  rnssopab 3825  ffnfv 3828  fsn 3834  fsn2 3836  fconstfv 3849  abianfp 3962  ersymb 4273  mapval2 4335  map0 4344  mapsn 4345  bren2 4389  en0 4423  en1 4426  pw2en 4446  canth2 4484  mapxpen 4495  xpmapenlem5 4500  0sdom1dom 4525  unfilem1 4548  fiint 4559  fiintOLD 4560  pwfiOLD 4571  sucprcreg 4600  opthreg 4604  suc11reg 4605  infeq5 4621  elom3 4631  isfiniteOLD 4634  rankr1 4674  rankonid 4695  rankeq0 4696  rankr1id 4697  rankuni 4698  rankxplim3 4714  scott0 4717  karden 4726  aceq3 4733  aceq4 4734  aceq5lem3 4737  aceq5 4740  aceq7 4743  ac9s 4764  kmlem2 4766  kmlem13 4777  fodomb 4800  brdom3 4801  brdom5 4802  brdom4 4803  brdom7disj 4804  brdom6disj 4805  oncard 4829  cardlim 4851  alephgeom 4882  iscard3 4888  cdainf 4937  reclem1pr 5156  mappsrpr 5218  map2psrpr 5220  supsrlem1 5225  supsrlem2 5226  addcan 5351  le2tri3 5589  ltadd2 5590  mulcan 5686  mulcanOLD 5687  mul0or 5694  rec11i 5777  eqneg 5804  ltmul1i 5821  nnsub 5956  dfn2 6112  elnnz 6145  elnn0z 6147  elnnz1 6155  elnn0nn 6171  elnnnn0b 6173  elnnnn0c 6174  nneo 6197  om2uzran 6300  elioo4g 6385  eluzfz2b 6490  elfz2nn0t 6495  sumsqne0 6634  nnesq 6662  nn0opth 6666  sqr0 6672  cru 6737  crne0 6739  negreb 6795  abs00 6842  abslt 6875  absle 6876  cau5 6919  cvg1 6921  cvg2 6922  cvg3 6923  cvganz 6924  climshft 7104  efltb 7407  dscmet 7918  xplm 7975  iscms2 7994  issubg 8116  nmlno0lem 8453  isblo3i 8461  blocni 8465  cosh111lem2 8715  circgrp 8740  hvsubeq0 8930  hvaddcan 8932  bcseq 8986  hlimreu 9110  hlimeu 9111  norm1ex 9122  hhsssh 9139  dfch2 9249  pjoc1 9264  pjch 9265  shlub 9346  shslub 9358  shs00 9373  chsscon3 9384  chlejb1 9399  chj00 9410  shjshsel 9416  h1de2ctlem 9478  spanunsn 9502  cmcm 9535  cmbr3 9543  cmbr4 9544  pjrn 9647  pj11 9656  hosubeq0 9752  dmadjrnb 9830  nmlnop0ALT 9920  lnopeq0 9932  elunop2t 9938  lnopcon 9963  lncnopbd 9966  lnfncon 9990  adjbdlnb 10017  adjbd1o 10018  adjeq0 10024  rnbra 10040  pjss1co 10091  pjss2co 10092  pjnormss 10096  pjssdif2 10102  pjssdif1 10103  pjhmopidm 10110  pjinvar 10119  pjin2 10121  pjc 10128  pjcmmul1 10129  pjcmmul2 10130  strb 10185  hstrb 10193  mdsl1 10248  atom1d 10280  chrelat2 10292  cvbr3 10294  cvexch 10296  sumdmd 10347  dmdbr4at 10348  dmdbr5at 10349  dmdbr6at 10350  dmdbr7at 10351  cdj3 10368  and4as 10432  and4com 10433  fiv 10482  fivOLD 10483  dtopcl 10615

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain