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  634  con2b  669  imnan  690  2false  701  pm5.21nii  704  pm4.8  707  oibabs  714  orcom  728  ioran  752  oridm  757  orbi2i  762  or12  766  pm4.44  779  ordi  816  andi  818  pm4.72  827  stdcndc  845  stdcndcOLD  846  stdcn  847  dcnn  848  pm4.82  950  rnlem  976  3jaob  1302  xoranor  1377  falantru  1403  3impexp  1437  3impexpbicom  1438  alcom  1478  19.26  1481  19.3h  1553  19.3  1554  19.21h  1557  19.43  1628  19.9h  1643  excom  1664  19.41h  1685  19.41  1686  equcom  1706  equsalh  1726  equsex  1728  cbvalv1  1751  cbvexv1  1752  cbvalh  1753  cbvexh  1755  sbbii  1765  sbh  1776  equs45f  1802  sb6f  1803  sbcof2  1810  sbequ8  1847  sbidm  1851  sb5rf  1852  sb6rf  1853  equvin  1863  sbimv  1893  cbvalvw  1919  cbvexvw  1920  sbalyz  1999  eu2  2070  eu3h  2071  eu5  2073  mo3h  2079  euan  2082  axext4  2161  cleqh  2277  r19.26  2603  ralcom3  2645  ceqsex  2777  gencbvex  2785  gencbvex2  2786  gencbval  2787  eqvinc  2862  pm13.183  2877  rr19.3v  2878  rr19.28v  2879  reu6  2928  reu3  2929  sbnfc2  3119  difdif  3262  ddifnel  3268  ddifstab  3269  ssddif  3371  difin  3374  uneqin  3388  indifdir  3393  undif3ss  3398  difrab  3411  un00  3471  undifss  3505  ssdifeq0  3507  ralidm  3525  ralf0  3528  ralm  3529  elpr2  3616  snidb  3624  difsnb  3737  preq12b  3772  preqsn  3777  axpweq  4173  exmidn0m  4203  exmidsssn  4204  exmid0el  4206  exmidel  4207  exmidundif  4208  exmidundifim  4209  sspwb  4218  unipw  4219  opm  4236  opth  4239  ssopab2b  4278  elon2  4378  unexb  4444  eusvnfb  4456  eusv2nf  4458  ralxfrALT  4469  uniexb  4475  iunpw  4482  onsucb  4504  unon  4512  sucprcreg  4550  opthreg  4557  ordsuc  4564  dcextest  4582  peano2b  4616  opelxp  4658  opthprc  4679  relop  4779  issetid  4783  xpid11  4852  elres  4945  iss  4955  issref  5013  xpmlem  5051  sqxpeq0  5054  ssrnres  5073  dfrel2  5081  relrelss  5157  fn0  5337  funssxp  5387  f00  5409  f0bi  5410  dffo2  5444  ffoss  5495  f1o00  5498  fo00  5499  fv3  5540  dff2  5662  dffo4  5666  dffo5  5667  fmpt  5668  ffnfv  5676  fsn  5690  fsn2  5692  isores1  5817  ssoprab2b  5934  eqfnov2  5984  cnvoprab  6237  reldmtpos  6256  mapsn  6692  mapsncnv  6697  mptelixpg  6736  elixpsn  6737  ixpsnf1o  6738  en0  6797  en1  6801  dom0  6840  exmidpw  6910  exmidpweq  6911  pw1fin  6912  undifdcss  6924  fidcenum  6957  djuexb  7045  ctssdc  7114  exmidomni  7142  nninfwlpo  7179  exmidfodomr  7205  exmidontri  7240  exmidontri2or  7244  onntri3or  7246  onntri2or  7247  dftap2  7252  exmidmotap  7262  elni2  7315  ltbtwnnqq  7416  enq0ref  7434  elnp1st2nd  7477  elrealeu  7830  elreal2  7831  le2tri3i  8068  elnn0nn  9220  elnnnn0b  9222  elnnnn0c  9223  elnnz  9265  elnn0z  9268  elnnz1  9278  elz2  9326  eluz2b2  9605  elnn1uz2  9609  elpqb  9651  elioo4g  9936  eluzfz2b  10035  fzm  10040  elfz1end  10057  fzass4  10064  elfz1b  10092  fz01or  10113  nn0fz0  10121  fzolb  10155  fzom  10166  elfzo0  10184  fzo1fzo0n0  10185  elfzo0z  10186  elfzo1  10192  rexanuz  10999  rexuz3  11001  sqrt0rlem  11014  fisum0diag  11451  fprod0diagfz  11638  infssuzex  11952  isprm6  12149  oddpwdclemdc  12175  nnoddn2prmb  12264  4sqlem4  12392  ennnfone  12428  ctinfom  12431  ctinf  12433  fnpr2ob  12764  dfgrp2  12907  dfgrp3m  12974  dfgrp3me  12975  isnsg3  13072  dvdsrzring  13532  tgclb  13604  xmetunirn  13897  2sqlem2  14501  bj-nnsn  14524  bdeq  14614  bdop  14666  bdunexb  14711  bj-2inf  14729  bj-nn0suc  14755  exmidsbth  14811  trirec0  14831  redc0  14844  reap0  14845  neap0mkv  14855