Theorem impbii 126

Description: Infer an equivalence from an implication and its converse. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem impbii

Step	Hyp	Ref	Expression
1		impbii.1	. 2 |- ( ph -> ps )
2		impbii.2	. 2 |- ( ps -> ph )
3		bi3 119	. 2 |- ( ( ph -> ps ) -> ( ( ps -> ph ) -> ( ph <-> ps ) ) )
4	1, 2, 3	mp2 16	1 |- ( ph <-> ps )

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-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bicom  140  biid  171  2th  174  pm5.74  179  bitri  184  bibi2i  227  bi2.04  248  pm5.4  249  imdi  250  impexp  263  ancom  266  pm4.45im  334  dfbi2  392  anass  405  pm5.32  457  jcab  611  notnotnot  643  con2b  679  imnan  701  2false  713  pm5.21nii  716  pm4.8  719  oibabs  726  orcom  740  ioran  764  oridm  769  orbi2i  774  or12  778  pm4.44  791  ordi  828  andi  830  pm4.72  839  stdcndc  857  stdcndcOLD  858  stdcn  859  dcnn  860  pm4.82  963  rnlem  989  3jaob  1343  xoranor  1426  falantru  1452  3impexp  1487  3impexpbicom  1488  alcom  1531  19.26  1534  19.3h  1606  19.3  1607  19.21h  1610  19.43  1681  19.9h  1696  excom  1716  19.41h  1737  19.41  1738  equcom  1758  equsalh  1778  equsex  1780  cbvalv1  1804  cbvexv1  1805  cbvalh  1806  cbvexh  1808  sbbii  1818  sbh  1829  equs45f  1855  sb6f  1856  sbcof2  1863  sbequ8  1900  sbidm  1904  sb5rf  1905  sb6rf  1906  equvin  1916  sbimv  1948  cbvalvw  1975  cbvexvw  1976  sbalyz  2059  eu2  2131  eu3h  2132  eu5  2134  mo3h  2140  euan  2143  axext4  2222  cleqh  2338  r19.26  2677  ralcom3  2719  ceqsex  2860  gencbvex  2869  gencbvex2  2870  gencbval  2871  eqvinc  2949  pm13.183  2964  rr19.3v  2965  rr19.28v  2966  reu6  3015  reu3  3016  sbnfc2  3208  difdif  3354  ddifnel  3360  ddifstab  3361  ssddif  3465  difin  3468  uneqin  3482  indifdir  3487  undif3ss  3492  difrab  3507  un00  3567  vvin  3569  undifss  3608  ssdifeq0  3610  ralidm  3628  ralf0  3630  ralm  3631  elpr2  3731  snidb  3739  rabsnifsb  3777  difsnb  3858  preq12b  3895  preqsn  3900  axpweq  4308  exmidn0m  4338  exmidsssn  4339  exmid0el  4341  exmidel  4342  exmidundif  4343  exmidundifim  4344  sspwb  4356  unipw  4357  opm  4374  opth  4377  ssopab2b  4419  elon2  4521  unexb  4588  eusvnfb  4600  eusv2nf  4602  ralxfrALT  4613  uniexb  4619  iunpw  4626  onsucb  4650  unon  4658  sucprcreg  4696  opthreg  4703  ordsuc  4710  dcextest  4728  peano2b  4762  opelxp  4804  opthprc  4826  relop  4930  issetid  4934  xpid11  5005  elres  5099  iss  5109  issref  5170  xpmlem  5208  sqxpeq0  5211  ssrnres  5230  dfrel2  5238  relrelss  5314  fn0  5503  funssxp  5557  f00  5584  f0bi  5585  dffo2  5619  ffoss  5672  f1o00  5676  fo00  5677  fv3  5718  dff2  5852  dffo4  5856  dffo5  5857  fmpt  5858  ffnfv  5866  fsn  5880  fsn2  5882  funop  5892  isores1  6020  ssoprab2b  6145  eqfnov2  6196  cnvoprab  6470  reldmtpos  6524  mapsn  6972  mapsncnv  6977  mptelixpg  7016  elixpsn  7017  ixpsnf1o  7018  en0  7082  en1  7086  modom  7108  dom0  7138  exmidpw  7215  exmidpweq  7216  pw1fin  7217  exmidpw2en  7219  undifdcss  7230  exmidssfi  7246  residfi  7254  fidcenum  7273  djuexb  7384  ctssdc  7453  exmidomni  7482  nninfinfwlpo  7520  nninfwlpo  7521  exmidfodomr  7556  iftrueb01  7582  exmidontri  7598  exmidontri2or  7602  onntri3or  7604  onntri2or  7605  dftap2  7617  exmidmotap  7627  elni2  7681  ltbtwnnqq  7782  enq0ref  7800  elnp1st2nd  7843  elrealeu  8196  elreal2  8197  le2tri3i  8434  elnn0nn  9605  elnnnn0b  9607  elnnnn0c  9608  elnnz  9654  elnn0z  9657  elnnz1  9667  elz2  9716  eluz2b2  10003  elnn1uz2  10007  elpqb  10050  elioo4g  10336  eluzfz2b  10437  fzm  10442  elfz1end  10461  fzass4  10468  elfz1b  10497  fz01or  10518  nn0fz0  10526  fzolb  10561  fzom  10572  elfzo0  10593  fzo1fzo0n0  10595  elfzo0z  10596  elfzo1  10603  infssuzex  10666  hashf1  11287  hash2en  11295  wrdexb  11316  0wrd0  11330  rexanuz  11754  rexuz3  11756  sqrt0rlem  11769  fisum0diag  12208  fprod0diagfz  12395  isprm6  12925  oddpwdclemdc  12951  nnoddn2prmb  13041  4sqlem4  13171  4sqexercise1  13177  ballotfilem2  13228  ballotfilemrinv  13277  ballotfilemth  13281  ennnfone  13316  ctinfom  13319  ctinf  13321  fnpr2ob  13661  dfgrp2  13832  dfgrp3m  13904  dfgrp3me  13905  isnsg3  14010  invghm  14133  dvdsrzring  14938  zrhval  14952  tgclb  15166  xmetunirn  15459  dich0  15753  elply2  15836  2sqlem2  16234  umgrislfupgrenlem  16371  umgrislfupgrdom  16372  uspgrupgrushgr  16423  usgrumgruspgr  16426  usgruspgrben  16427  usgrislfuspgrdom  16431  clwwlkn1loopb  16661  dichmul0or  16760  bj-nnsn  16761  bdeq  16849  bdop  16901  bdunexb  16946  bj-2inf  16964  bj-nn0suc  16990  pw1dceq  17035  exmidnotnotr  17036  exmidcon  17037  exmidpeirce  17038  wexmiddiffi  17044  wexmiddifxy  17046  nnnninfen  17064  exmidsbth  17069  trirec0  17093  redc0  17107  reap0  17108  cndcap  17109  neap0mkv  17119