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 424  pm4.43 433  anidm 434  ancom 437  imdistan 444  pm5.3 448  pm5.61 449  abai 481  anbi2i 482  anabs1 494  anabs7 496  orabs 583  pm5.74 585  ordi 598  pm4.71 637  pm4.72 643  oibabs 656  pm5.18 662  mt2bi 715  2th 720  bianfi 739  pm4.82 741  orbidi 745  consensus 769  19.3 1033  alcom 1034  19.9 1038  excom 1048  19.21 1058  19.23 1065  19.26 1069  equcom 1131  equsal 1153  sbbii 1176  sbf 1188  sb6x 1190  equs45f 1202  sb6f 1203  dfsb2 1227  sbn 1233  sbim 1236  sb5rf 1261  sb6rf 1262  sb8 1263  sb9 1266  equvin 1277  mo 1395  eu2 1398  mo2 1402  exmoeu 1415  2mo 1450  2eu6 1457  ralcom3 1780  rabab 1825  ceqsex 1837  gencbvex2 1842  euxfr2 1929  reu3 1934  reu6 1935  sspss 2148  ssin 2235  unineq 2258  uneqin 2259  difrab 2276  un00 2310  vss 2311  ralf0 2363  elpr2 2429  snidb 2438  disjsn 2445  pwpw0 2473  prss 2475  sssn 2477  sspr 2479  tpss 2480  preq12b 2487  preqsn 2490  pwsnALT 2505  iununi 2621  intex 2734  intnex 2735  iin0 2745  sspwb 2761  sspwuni 2764  opth 2793  opprc1b 2802  opprc3 2803  opthwiener 2813  ssopab2 2828  pwssun 2833  pwundif 2834  unexb 2879  ralxfr 2905  reuxfr2 2909  uniexb 2913  iunpw 2920  dfwe2 2941  elon2 2965  ordeleqon 2996  onintrab 3019  unon 3094  onuninsuc 3114  ordzsl 3122  dflim3 3124  ralxp 3224  opthprc 3227  relop 3281  issetid 3286  xpid11 3341  iss 3403  cotr 3442  cnvsym 3443  asymref2 3446  xpnz 3472  ssrnres 3487  dfrel2 3491  unixp0 3524  dffun7 3546  fn0 3611  fnopabg 3621  fnf 3634  funssxp 3644  f00 3663  dffo2 3681  f1o2 3699  ffoss 3717  f1o00 3720  fo00 3721  fv3 3739  fnopabfv 3764  dff4 3822  dff2 3823  dffo4 3826  dffo5 3827  exfo 3828  fopab2 3829  rnssopab 3831  ffnfv 3834  fsn 3840  fsn2 3842  fconstfv 3855  abianfp 3968  ersymb 4279  mapval2 4341  map0 4350  mapsn 4351  bren2 4395  en0 4429  en1 4432  pw2en 4452  canth2 4490  mapxpen 4501  xpmapenlem5 4506  0sdom1dom 4530  unfilem1 4560  fiint 4572  fiintOLD 4573  pwfi 4579  pwfiOLD 4580  sucprcreg 4609  opthreg 4613  suc11reg 4614  infeq5 4630  elom3 4640  isfinite 4643  isfiniteOLD 4644  rankr1 4684  rankonid 4705  rankeq0 4706  rankr1id 4707  rankuni 4708  rankxplim3 4724  scott0 4727  karden 4736  aceq3 4743  aceq4 4744  aceq5lem3 4747  aceq5 4750  aceq7 4753  ac9s 4774  kmlem2 4776  kmlem13 4787  fodomb 4810  brdom3 4811  brdom5 4812  brdom4 4813  brdom7disj 4814  brdom6disj 4815  oncard 4839  cardlim 4862  alephgeom 4893  iscard3 4899  cdainf 4949  reclem1pr 5168  mappsrpr 5230  map2psrpr 5232  supsrlem1 5237  supsrlem2 5238  addcan 5363  le2tri3 5601  ltadd2 5602  mulcan 5698  mulcanOLD 5699  mul0or 5706  rec11i 5779  eqneg 5806  ltmul1i 5823  nnsub 5958  dfn2 6114  elnnz 6147  elnn0z 6149  elnnz1 6157  elnn0nn 6173  elnnnn0b 6175  elnnnn0c 6176  nneo 6199  om2uzran 6301  elioo4g 6386  eluzfz2b 6491  elfz2nn0t 6496  sumsqne0 6635  nnesq 6663  nn0opth 6667  sqr0 6673  cru 6738  crne0 6740  negreb 6795  abs00 6842  abslt 6875  absle 6876  cau5 6919  cvg1 6921  cvg2 6922  cvg3 6923  cvganz 6924  climshft 7104  efltb 7407  dscmet 7915  xplm 7972  iscms2 7991  issubg 8112  nmlno0lem 8449  isblo3i 8457  blocni 8461  cosh111lem2 8710  circgrp 8735  hvsubeq0 8925  hvaddcan 8927  bcseq 8981  hlimreu 9105  hlimeu 9106  norm1ex 9117  hhsssh 9134  dfch2 9244  pjoc1 9259  pjch 9260  shlub 9341  shslub 9353  shs00 9368  chsscon3 9379  chlejb1 9394  chj00 9405  shjshsel 9411  h1de2ctlem 9473  spanunsn 9497  cmcm 9530  cmbr3 9538  cmbr4 9539  pjrn 9642  pj11 9651  hosubeq0 9747  dmadjrnb 9825  nmlnop0ALT 9915  lnopeq0 9927  elunop2t 9933  lnopcon 9958  lncnopbd 9961  lnfncon 9985  adjbdlnb 10012  adjbd1o 10013  adjeq0 10019  rnbra 10035  pjss1co 10086  pjss2co 10087  pjnormss 10091  pjssdif2 10097  pjssdif1 10098  pjhmopidm 10105  pjinvar 10114  pjin2 10116  pjc 10123  pjcmmul1 10124  pjcmmul2 10125  strb 10180  hstrb 10188  mdsl1 10243  atom1d 10275  chrelat2 10287  cvbr3 10289  cvexch 10291  sumdmd 10342  dmdbr4at 10343  dmdbr5at 10344  dmdbr6at 10345  dmdbr7at 10346  cdj3 10363  and4as 10427  and4com 10428  fiv 10470  dtopcl 10586

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