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 )

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced 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  388  anass  401  pm5.32  453  jcab  603  notnotnot  635  con2b  670  imnan  691  2false  702  pm5.21nii  705  pm4.8  708  oibabs  715  orcom  729  ioran  753  oridm  758  orbi2i  763  or12  767  pm4.44  780  ordi  817  andi  819  pm4.72  828  stdcndc  846  stdcndcOLD  847  stdcn  848  dcnn  849  pm4.82  952  rnlem  978  3jaob  1313  xoranor  1388  falantru  1414  3impexp  1448  3impexpbicom  1449  alcom  1489  19.26  1492  19.3h  1564  19.3  1565  19.21h  1568  19.43  1639  19.9h  1654  excom  1675  19.41h  1696  19.41  1697  equcom  1717  equsalh  1737  equsex  1739  cbvalv1  1762  cbvexv1  1763  cbvalh  1764  cbvexh  1766  sbbii  1776  sbh  1787  equs45f  1813  sb6f  1814  sbcof2  1821  sbequ8  1858  sbidm  1862  sb5rf  1863  sb6rf  1864  equvin  1874  sbimv  1905  cbvalvw  1931  cbvexvw  1932  sbalyz  2015  eu2  2086  eu3h  2087  eu5  2089  mo3h  2095  euan  2098  axext4  2177  cleqh  2293  r19.26  2620  ralcom3  2662  ceqsex  2798  gencbvex  2807  gencbvex2  2808  gencbval  2809  eqvinc  2884  pm13.183  2899  rr19.3v  2900  rr19.28v  2901  reu6  2950  reu3  2951  sbnfc2  3142  difdif  3285  ddifnel  3291  ddifstab  3292  ssddif  3394  difin  3397  uneqin  3411  indifdir  3416  undif3ss  3421  difrab  3434  un00  3494  undifss  3528  ssdifeq0  3530  ralidm  3548  ralf0  3550  ralm  3551  elpr2  3641  snidb  3649  difsnb  3762  preq12b  3797  preqsn  3802  axpweq  4201  exmidn0m  4231  exmidsssn  4232  exmid0el  4234  exmidel  4235  exmidundif  4236  exmidundifim  4237  sspwb  4246  unipw  4247  opm  4264  opth  4267  ssopab2b  4308  elon2  4408  unexb  4474  eusvnfb  4486  eusv2nf  4488  ralxfrALT  4499  uniexb  4505  iunpw  4512  onsucb  4536  unon  4544  sucprcreg  4582  opthreg  4589  ordsuc  4596  dcextest  4614  peano2b  4648  opelxp  4690  opthprc  4711  relop  4813  issetid  4817  xpid11  4886  elres  4979  iss  4989  issref  5049  xpmlem  5087  sqxpeq0  5090  ssrnres  5109  dfrel2  5117  relrelss  5193  fn0  5374  funssxp  5424  f00  5446  f0bi  5447  dffo2  5481  ffoss  5533  f1o00  5536  fo00  5537  fv3  5578  dff2  5703  dffo4  5707  dffo5  5708  fmpt  5709  ffnfv  5717  fsn  5731  fsn2  5733  isores1  5858  ssoprab2b  5976  eqfnov2  6027  cnvoprab  6289  reldmtpos  6308  mapsn  6746  mapsncnv  6751  mptelixpg  6790  elixpsn  6791  ixpsnf1o  6792  en0  6851  en1  6855  dom0  6896  exmidpw  6966  exmidpweq  6967  pw1fin  6968  exmidpw2en  6970  undifdcss  6981  residfi  7001  fidcenum  7017  djuexb  7105  ctssdc  7174  exmidomni  7203  nninfwlpo  7240  exmidfodomr  7266  exmidontri  7301  exmidontri2or  7305  onntri3or  7307  onntri2or  7308  dftap2  7313  exmidmotap  7323  elni2  7376  ltbtwnnqq  7477  enq0ref  7495  elnp1st2nd  7538  elrealeu  7891  elreal2  7892  le2tri3i  8130  elnn0nn  9285  elnnnn0b  9287  elnnnn0c  9288  elnnz  9330  elnn0z  9333  elnnz1  9343  elz2  9391  eluz2b2  9671  elnn1uz2  9675  elpqb  9718  elioo4g  10003  eluzfz2b  10102  fzm  10107  elfz1end  10124  fzass4  10131  elfz1b  10159  fz01or  10180  nn0fz0  10188  fzolb  10223  fzom  10234  elfzo0  10252  fzo1fzo0n0  10253  elfzo0z  10254  elfzo1  10260  wrdexb  10929  0wrd0  10943  rexanuz  11135  rexuz3  11137  sqrt0rlem  11150  fisum0diag  11587  fprod0diagfz  11774  infssuzex  12089  isprm6  12288  oddpwdclemdc  12314  nnoddn2prmb  12403  4sqlem4  12533  4sqexercise1  12539  ennnfone  12585  ctinfom  12588  ctinf  12590  fnpr2ob  12926  dfgrp2  13102  dfgrp3m  13174  dfgrp3me  13175  isnsg3  13280  invghm  13402  dvdsrzring  14102  zrhval  14116  tgclb  14244  xmetunirn  14537  dich0  14831  elply2  14914  2sqlem2  15272  bj-nnsn  15295  bdeq  15385  bdop  15437  bdunexb  15482  bj-2inf  15500  bj-nn0suc  15526  nnnninfen  15581  exmidsbth  15584  trirec0  15604  redc0  15617  reap0  15618  cndcap  15619  neap0mkv  15629