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  607  notnotnot  639  con2b  675  imnan  697  2false  709  pm5.21nii  712  pm4.8  715  oibabs  722  orcom  736  ioran  760  oridm  765  orbi2i  770  or12  774  pm4.44  787  ordi  824  andi  826  pm4.72  835  stdcndc  853  stdcndcOLD  854  stdcn  855  dcnn  856  pm4.82  959  rnlem  985  3jaob  1339  xoranor  1422  falantru  1448  3impexp  1483  3impexpbicom  1484  alcom  1527  19.26  1530  19.3h  1602  19.3  1603  19.21h  1606  19.43  1677  19.9h  1692  excom  1712  19.41h  1733  19.41  1734  equcom  1754  equsalh  1774  equsex  1776  cbvalv1  1800  cbvexv1  1801  cbvalh  1802  cbvexh  1804  sbbii  1814  sbh  1825  equs45f  1851  sb6f  1852  sbcof2  1859  sbequ8  1896  sbidm  1900  sb5rf  1901  sb6rf  1902  equvin  1912  sbimv  1944  cbvalvw  1971  cbvexvw  1972  sbalyz  2055  eu2  2127  eu3h  2128  eu5  2130  mo3h  2136  euan  2139  axext4  2218  cleqh  2334  r19.26  2671  ralcom3  2713  ceqsex  2854  gencbvex  2863  gencbvex2  2864  gencbval  2865  eqvinc  2943  pm13.183  2958  rr19.3v  2959  rr19.28v  2960  reu6  3009  reu3  3010  sbnfc2  3202  difdif  3348  ddifnel  3354  ddifstab  3355  ssddif  3459  difin  3462  uneqin  3476  indifdir  3481  undif3ss  3486  difrab  3499  un00  3559  undifss  3594  ssdifeq0  3596  ralidm  3614  ralf0  3616  ralm  3617  elpr2  3716  snidb  3724  rabsnifsb  3762  difsnb  3842  preq12b  3879  preqsn  3884  axpweq  4289  exmidn0m  4319  exmidsssn  4320  exmid0el  4322  exmidel  4323  exmidundif  4324  exmidundifim  4325  sspwb  4337  unipw  4338  opm  4355  opth  4358  ssopab2b  4400  elon2  4502  unexb  4568  eusvnfb  4580  eusv2nf  4582  ralxfrALT  4593  uniexb  4599  iunpw  4606  onsucb  4630  unon  4638  sucprcreg  4676  opthreg  4683  ordsuc  4690  dcextest  4708  peano2b  4742  opelxp  4784  opthprc  4806  relop  4910  issetid  4914  xpid11  4985  elres  5079  iss  5089  issref  5150  xpmlem  5188  sqxpeq0  5191  ssrnres  5210  dfrel2  5218  relrelss  5294  fn0  5483  funssxp  5537  f00  5564  f0bi  5565  dffo2  5599  ffoss  5652  f1o00  5656  fo00  5657  fv3  5698  dff2  5826  dffo4  5830  dffo5  5831  fmpt  5832  ffnfv  5840  fsn  5854  fsn2  5856  funop  5866  isores1  5993  ssoprab2b  6118  eqfnov2  6169  cnvoprab  6443  reldmtpos  6497  mapsn  6938  mapsncnv  6943  mptelixpg  6982  elixpsn  6983  ixpsnf1o  6984  en0  7048  en1  7052  modom  7074  dom0  7104  exmidpw  7181  exmidpweq  7182  pw1fin  7183  exmidpw2en  7185  undifdcss  7196  exmidssfi  7212  residfi  7220  fidcenum  7239  djuexb  7348  ctssdc  7417  exmidomni  7446  nninfinfwlpo  7484  nninfwlpo  7485  exmidfodomr  7520  iftrueb01  7546  exmidontri  7562  exmidontri2or  7566  onntri3or  7568  onntri2or  7569  dftap2  7581  exmidmotap  7591  elni2  7645  ltbtwnnqq  7746  enq0ref  7764  elnp1st2nd  7807  elrealeu  8160  elreal2  8161  le2tri3i  8398  elnn0nn  9555  elnnnn0b  9557  elnnnn0c  9558  elnnz  9604  elnn0z  9607  elnnz1  9617  elz2  9666  eluz2b2  9953  elnn1uz2  9957  elpqb  10000  elioo4g  10286  eluzfz2b  10387  fzm  10392  elfz1end  10410  fzass4  10417  elfz1b  10446  fz01or  10467  nn0fz0  10475  fzolb  10510  fzom  10521  elfzo0  10542  fzo1fzo0n0  10544  elfzo0z  10545  elfzo1  10552  infssuzex  10615  hash2en  11240  wrdexb  11261  0wrd0  11275  rexanuz  11698  rexuz3  11700  sqrt0rlem  11713  fisum0diag  12152  fprod0diagfz  12339  isprm6  12869  oddpwdclemdc  12895  nnoddn2prmb  12985  4sqlem4  13115  4sqexercise1  13121  ballotfilem2  13172  ballotfilemrinv  13221  ballotfilemth  13225  ennnfone  13260  ctinfom  13263  ctinf  13265  fnpr2ob  13604  dfgrp2  13782  dfgrp3m  13854  dfgrp3me  13855  isnsg3  13960  invghm  14082  dvdsrzring  14877  zrhval  14891  tgclb  15056  xmetunirn  15349  dich0  15643  elply2  15726  2sqlem2  16114  umgrislfupgrenlem  16251  umgrislfupgrdom  16252  uspgrupgrushgr  16303  usgrumgruspgr  16306  usgruspgrben  16307  usgrislfuspgrdom  16311  clwwlkn1loopb  16541  bj-nnsn  16631  bdeq  16719  bdop  16771  bdunexb  16816  bj-2inf  16834  bj-nn0suc  16860  pw1dceq  16904  exmidnotnotr  16905  exmidcon  16906  exmidpeirce  16907  nnnninfen  16925  exmidsbth  16930  trirec0  16954  redc0  16968  reap0  16969  cndcap  16970  neap0mkv  16981