Theorem impbii 155

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

Hypotheses

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

Assertion

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

Proof of Theorem impbii

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

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

This theorem is referenced by:  dfbi1 156  bi2.04 158  notnot 159  pm4.8 160  pm4.81 161  con1b 162  con2b 163  con34b 164  pm5.4 165  imdi 166  pm5.41 167  biid 168  bicomi 170  bitri 171  imbi2i 183  imbi1i 184  notbii 185  a1bi 195  con1bii 218  dfor2 227  oridm 241  anclb 327  ancrb 328  pm4.45im 330  pm4.44 343  pm5.63 344  impexp 345  jaob 422  pm4.43 432  anidm 433  ancom 437  imdistan 444  pm5.3 448  pm5.61 449  abai 482  anbi2i 483  anabs1 495  anabs7 497  orabs 584  pm5.74 586  ordi 599  pm4.71 638  pm4.72 644  oibabs 657  pm5.18 663  mt2bi 718  2th 723  bianfi 742  pm4.82 744  orbidi 748  consensus 772  dn1 779  19.3 1067  alcom 1068  19.9 1072  excom 1082  19.21 1092  19.23 1099  19.26 1103  equcom 1166  equsal 1188  sbbii 1211  sbf 1223  sb6x 1225  equs45f 1237  sb6f 1238  dfsb2 1262  sbn 1268  sbim 1271  sb5rf 1297  sb6rf 1298  sb8 1299  sb9 1302  equvin 1313  mo 1432  eu2 1435  mo2 1439  exmoeu 1452  2mo 1487  2eu6 1494  axext4 1503  nebi 1678  ralcom3 1823  rabab 1868  ceqsex 1880  gencbvex2 1885  euxfr2 1972  reu3 1977  reu6 1978  sspss 2197  ssin 2284  unineq 2307  uneqin 2308  difrab 2325  un00 2359  vss 2360  ralf0 2413  elpr2 2483  snidb 2495  disjsn 2502  pwpw0 2533  prss 2536  sssn 2538  sspr 2540  tpss 2541  preq12b 2548  preqsn 2551  pwsnALT 2566  iununi 2686  intex 2803  intnex 2804  iin0 2814  axpweq 2817  sspwb 2835  unipw 2836  opth 2863  opprc1b 2872  opprc3 2873  opthwiener 2884  ssopab2 2900  pwssun 2905  pwundif 2906  elon2 2986  unexb 3096  ralxfr 3122  reuxfr2 3126  uniexb 3130  iunpw 3137  dfwe2 3140  ordeleqon 3144  onintrab 3158  unon 3185  onuninsuci 3194  ordzsl 3199  dflim3 3201  ralxp 3301  opthprc 3306  relop 3365  issetid 3370  xpid11 3422  iss 3487  cotr 3528  cnvsym 3529  asymref2 3532  xpnz 3551  ssrnres 3566  dfrel2 3569  relrelss 3618  unixp0 3623  dffun8 3645  fn0 3711  fnopabg 3722  dffn2 3735  funssxp 3745  f00 3764  dffo2 3783  dff1o2 3801  ffoss 3822  f1o00 3825  fo00 3826  fv3 3844  dffn5 3869  dff2 3930  dff3 3931  dffo4 3934  dffo5 3935  exfo 3936  fopab2 3937  rnssopab 3939  ffnfv 3942  fsn 3948  fsn2 3950  fconstfv 3963  abianfp 4263  ersymb 4413  mapval2 4476  map0 4485  mapsn 4486  bren2 4530  en0 4564  en1 4567  pw2en 4587  canth2 4629  mapxpen 4642  xpmapenlem5 4647  0sdom1dom 4671  unfilem1 4694  fiint 4703  pwfi 4714  sucprcreg 4743  opthreg 4749  suc11reg 4750  infeq5 4766  elom3 4777  isfinite 4780  rankr1 4820  rankonid 4841  rankeq0 4842  rankr1id 4843  rankuni 4844  rankxplim3 4860  scott0 4863  karden 4872  aceq3 4879  aceq4 4880  aceq5lem3 4883  aceq5 4886  aceq7 4889  ac9s 4910  kmlem2 4912  kmlem13 4923  fodomb 4946  brdom3 4947  brdom5 4948  brdom4 4949  brdom7disj 4950  brdom6disj 4951  oncard 4976  cardlim 5001  alephgeom 5032  iscard3 5038  cdainf 5089  reclem1pr 5310  mappsrpr 5372  map2psrpr 5374  supsrlem1 5379  supsrlem2 5380  addcani 5505  le2tri3i 5743  ltadd2i 5744  mulcani 5842  mul0ori 5846  rec11ii 5916  eqnegi 5944  ltmul1ii 5961  nnsubi 6102  dfn2 6280  elnnz 6313  elnn0z 6315  elnnz1 6323  elnn0nn 6339  elnnnn0b 6341  elnnnn0c 6342  nneoi 6368  elioo4g 6511  eluzfz2b 6618  elfz2nn0 6625  om2uzrani 6663  sumsqne0i 6831  nnesqi 6863  nn0opthi 6867  sqr0 6873  crui 6938  crne0i 6940  negrebi 6996  abs00i 7044  abslti 7078  abslei 7079  cau5i 7122  cvg1 7124  cvg2i 7125  cvg3i 7126  cvganz 7127  climshfti 7307  efltbi 7615  dscmet 8129  xplm 8186  iscms2 8205  issubg 8358  nmlno0lem 8708  isblo3i 8716  blocni 8720  cosh111lem2 8987  circgrp 9012  grothpw 9054  hvsubeq0i 9205  hvaddcani 9207  bcseqi 9262  hlimreui 9386  hlimeui 9387  norm1exi 9398  hhsssh 9415  dfch2 9525  pjoc1i 9540  pjchi 9541  shlubi 9622  shslubi 9634  shs00i 9649  chsscon3i 9660  chlejb1i 9675  chj00i 9686  shjshseli 9692  h1de2ctlem 9754  spanunsni 9778  cmcmi 9811  cmbr3i 9819  cmbr4i 9820  pjrni 9925  pj11i 9934  hosubeq0i 10032  dmadjrnb 10110  nmlnop0iALT 10199  lnopeq0i 10211  elunop2 10217  lnopconi 10242  lncnopbd 10245  lnfnconi 10269  adjbdlnb 10296  adjbd1o 10297  adjeq0 10303  rnbra 10320  pjss1coi 10371  pjss2coi 10372  pjnormssi 10376  pjssdif2i 10382  pjssdif1i 10383  pjhmopidm 10390  pjinvari 10400  pjin2i 10402  pjci 10409  pjcmmul1i 10410  pjcmmul2i 10411  strbi 10466  hstrbi 10474  mdsl1i 10529  atom1d 10561  chrelat2i 10573  cvbr3i 10575  cvexchi 10577  sumdmdi 10629  dmdbr4ati 10630  dmdbr5ati 10631  dmdbr6ati 10632  dmdbr7ati 10633  cdj3i 10650  xfree 10653  and4as 10716  and4com 10717  anddi2 10718  ref3w 10772  domleqt 10792  fldleqt 10795  restidsing 10805  fiv 10849  definc 10869  domncnt 10872  ranncnt 10873  zrdivrng 10969  sallnei 11016  subspemp 11060  dtopcl 11107  clindistop 11131  singempcon 11134  bsi3 11140  altretoplem2 11143  altretop 11144  r19.2zb 11393  alexsub 11500  is2ndc2 11534  topbasfne 11560  filnetlem1 11763  gapmlem 11783  difxp 11798  oprabopabf 11807  elnnr 11874

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 145

Copyright terms: Public domain