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  4310  exmidn0m  4340  exmidsssn  4341  exmid0el  4343  exmidel  4344  exmidundif  4345  exmidundifim  4346  sspwb  4358  unipw  4359  opm  4376  opth  4379  ssopab2b  4421  elon2  4523  unexb  4590  eusvnfb  4602  eusv2nf  4604  ralxfrALT  4615  uniexb  4621  iunpw  4628  onsucb  4652  unon  4660  sucprcreg  4698  opthreg  4705  ordsuc  4712  dcextest  4730  peano2b  4764  opelxp  4806  opthprc  4828  relop  4932  issetid  4936  xpid11  5007  elres  5101  iss  5112  issref  5173  xpmlem  5211  sqxpeq0  5214  ssrnres  5233  dfrel2  5241  relrelss  5317  fn0  5506  funssxp  5560  f00  5587  f0bi  5588  dffo2  5622  ffoss  5675  f1o00  5679  fo00  5680  fv3  5721  dff2  5855  dffo4  5859  dffo5  5860  fmpt  5861  ffnfv  5869  fsn  5883  fsn2  5885  funop  5895  isores1  6023  ssoprab2b  6148  eqfnov2  6199  cnvoprab  6474  reldmtpos  6528  mapsn  6976  mapsncnv  6981  mptelixpg  7020  elixpsn  7021  ixpsnf1o  7022  en0  7086  en1  7090  modom  7112  dom0  7142  exmidpw  7219  exmidpweq  7220  pw1fin  7221  exmidpw2en  7223  undifdcss  7234  exmidssfi  7250  residfi  7258  fidcenum  7278  djuexb  7390  ctssdc  7459  exmidomni  7488  nninfinfwlpo  7526  nninfwlpo  7527  exmidfodomr  7562  iftrueb01  7588  exmidontri  7604  exmidontri2or  7608  onntri3or  7610  onntri2or  7611  dftap2  7623  exmidmotap  7633  elni2  7687  ltbtwnnqq  7788  enq0ref  7806  elnp1st2nd  7849  elrealeu  8202  elreal2  8203  le2tri3i  8441  elnn0nn  9616  elnnnn0b  9618  elnnnn0c  9619  elnnz  9665  elnn0z  9668  elnnz1  9678  elz2  9727  eluz2b2  10019  elnn1uz2  10023  elpqb  10067  elioo4g  10353  eluzfz2b  10454  fzm  10459  elfz1end  10478  fzass4  10485  elfz1b  10514  fz01or  10535  nn0fz0  10543  fzolb  10578  fzom  10589  elfzo0  10610  fzo1fzo0n0  10612  elfzo0z  10613  elfzo1  10620  infssuzex  10683  hashf1  11309  hash2en  11317  wrdexb  11338  0wrd0  11352  rexanuz  11776  rexuz3  11778  sqrt0rlem  11791  fisum0diag  12233  fprod0diagfz  12420  isprm6  12951  nnoddn2prmb  13070  4sqlem4  13200  4sqexercise1  13206  ballotfilem2  13286  ballotfilemrinv  13335  ballotfilemth  13339  ennnfone  13374  ctinfom  13377  ctinf  13379  fnpr2ob  13720  dfgrp2  13891  dfgrp3m  13963  dfgrp3me  13964  isnsg3  14069  invghm  14223  dvdsrzring  15047  zrhval  15061  tgclb  15291  xmetunirn  15584  dich0  15878  elply2  15961  2sqlem2  16439  umgrislfupgrenlem  16576  umgrislfupgrdom  16577  uspgrupgrushgr  16628  usgrumgruspgr  16631  usgruspgrben  16632  usgrislfuspgrdom  16636  clwwlkn1loopb  16866  dichmul0or  16965  bj-nnsn  16966  bdeq  17054  bdop  17106  bdunexb  17151  bj-2inf  17169  bj-nn0suc  17195  pw1dceq  17240  exmidnotnotr  17241  exmidcon  17242  exmidpeirce  17243  wexmiddiffi  17249  wexmiddifxy  17251  idjudju  17252  nnnninfen  17270  exmidsbth  17275  trirec0  17300  redc0  17314  reap0  17315  cndcap  17316  neap0mkv  17326