Theorem impbi 139

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 132	. 2 |- ((ph -> ps) -> ((ps -> ph) -> (ph <-> ps)))
4	1, 2, 3	mp2 43	1 |- (ph <-> ps)

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  bii 140  bi2.04 141  pm4.13 142  pm4.1 143  bi2.03 144  bi2.15 145  pm5.4 146  imdi 147  pm4.2 148  bicomi 150  bitr 151  imbi2i 160  imbi1i 161  negbii 162  a1bi 172  bicon1i 193  dfor2 199  oridm 208  anclb 264  ancrb 265  pm4.45im 267  impexp 276  jaob 328  anidm 331  ancom 333  imdistan 339  abai 366  anbi2i 367  anabs1 374  anabs7 376  oel 441  pm5.74 442  ordi 452  pm4.71 481  pm4.72 485  oibabs 493  pm5.18 497  orbidi 510  mt2bi 535  2th 540  tbt 541  nbn 542  bianfi 553  consensus 574  19.3r 714  alcom 715  19.9r 718  excom 728  19.21 738  19.23 745  19.26 749  eqcomb 812  eqsal 833  bisb 855  sbf 870  sb6x 871  sb6y 872  sbn 882  sbim 886  sb5f1 917  sb8 918  sb9 921  eqvin 932  mo 1020  eu2 1023  mo2 1026  exmoeu 1039  2eu4 1070  ralcom3 1315  rabab 1359  ceqsex 1370  alexeq 1409  elab3g 1420  euxfr2 1435  sbcie 1455  zfrep2 1475  sspss 1569  reuxfr2 1579  ssin 1659  unineq 1680  difrab 1695  ss0b 1726  un00 1728  vss 1729  snidb 1829  disjsn 1836  sssn 1852  prss 1854  tpss 1855  sspwb 1863  preq12b 1874  pwpw0 1883  opth 1898  opprc1b 1906  opprc3 1908  opthwiener 1914  pwssun 1917  unexb 1950  uniexb 1962  intex 1986  iununi 2037  iunpw 2040  ssopab2 2119  dfwe2 2187  elon2 2210  ordeleqon 2241  onintrab 2268  unon 2338  onuninsuc 2356  ordzsl 2366  dflim3 2368  ralxp 2456  opthprc 2457  iss 2599  cotr 2625  cnvsym 2626  dfrel2 2660  dffun7 2688  fn0 2739  fnopabg 2745  fnf 2753  f00 2773  f1o2 2804  ffoss 2820  f1o00 2823  fv3 2839  fnopabfv 2858  fopab2 2891  ffnfv 2892  fsn 2895  fsn2 2896  fconst2 2902  fconstfv 2903  abianfp 3000  fnoprab 3038  ersymb 3210  map0 3268  mapsn 3269  bren2 3293  en0 3328  en1 3331  pw2en 3348  0sdom 3368  canth2 3381  mapxpen 3390  xpmapenlem5 3395  0sdom1dom 3420  unfilem1 3438  fiint 3445  sucprcreg 3451  suc11reg 3456  inf5 3472  elom3 3478  isfinite 3480  rankr1 3518  rankonid 3538  rankr1id 3539  scott0 3542  karden 3551  aceq3 3556  aceq4 3557  aceq5lem3 3560  aceq5 3563  aceq7 3566  kmlem2 3581  kmlem12 3591  fodomb 3615  oncard 3636  cardlim 3657  alephgeom 3687  iscard3 3693  cdainf 3731  reclem1pr 3950  mappsrpr 4012  map2psrpr 4014  supsrlem1 4019  supsrlem2 4020  addcan 4120  subeq0 4163  mulcan 4207  mul0or 4210  rec11i 4261  le2tri3 4311  ltadd2 4312  eqneg 4378  ltmul1i 4393  nnsub 4450  elnnz 4572  elnn0z 4574  elnnz1 4581  elnn0nn 4593  om2uzran 4655  nneo 4719  nnesq 4720  nn0opth 4724  sqr0 4730  reim0 4809  rere 4810  negre 4825  abs00 4839  absgt0 4842  abslt 4855  absle 4856  hvsubeq0 5035  hvaddcan 5037  bcseq 5073  hlimreu 5145  hlimeu 5146  dfch2 5254  pjoc1 5268  pjch 5269  shlub 5347  shslub 5359  chsscon3 5383  chlejb1 5397  chj00 5408  shjshsel 5413  h1de2ctlem 5460  spanunsn 5482  cmcm 5501  cmbr3 5509  cmbr4 5510  pjrn 5587  pj11 5591  pjss1co 5633  pjss2co 5634  pjnormss 5638  pjin2 5647  pjc 5654  strb 5699  atom1d 5750  chrelat2 5758  cvexch 5760  sumdmd 5787

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

This theorem depends on definitions:  df-bi 128

metamath.org