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  1492  19.26  1495  19.3h  1567  19.3  1568  19.21h  1571  19.43  1642  19.9h  1657  excom  1678  19.41h  1699  19.41  1700  equcom  1720  equsalh  1740  equsex  1742  cbvalv1  1765  cbvexv1  1766  cbvalh  1767  cbvexh  1769  sbbii  1779  sbh  1790  equs45f  1816  sb6f  1817  sbcof2  1824  sbequ8  1861  sbidm  1865  sb5rf  1866  sb6rf  1867  equvin  1877  sbimv  1908  cbvalvw  1934  cbvexvw  1935  sbalyz  2018  eu2  2089  eu3h  2090  eu5  2092  mo3h  2098  euan  2101  axext4  2180  cleqh  2296  r19.26  2623  ralcom3  2665  ceqsex  2801  gencbvex  2810  gencbvex2  2811  gencbval  2812  eqvinc  2887  pm13.183  2902  rr19.3v  2903  rr19.28v  2904  reu6  2953  reu3  2954  sbnfc2  3145  difdif  3289  ddifnel  3295  ddifstab  3296  ssddif  3398  difin  3401  uneqin  3415  indifdir  3420  undif3ss  3425  difrab  3438  un00  3498  undifss  3532  ssdifeq0  3534  ralidm  3552  ralf0  3554  ralm  3555  elpr2  3645  snidb  3653  difsnb  3766  preq12b  3801  preqsn  3806  axpweq  4205  exmidn0m  4235  exmidsssn  4236  exmid0el  4238  exmidel  4239  exmidundif  4240  exmidundifim  4241  sspwb  4250  unipw  4251  opm  4268  opth  4271  ssopab2b  4312  elon2  4412  unexb  4478  eusvnfb  4490  eusv2nf  4492  ralxfrALT  4503  uniexb  4509  iunpw  4516  onsucb  4540  unon  4548  sucprcreg  4586  opthreg  4593  ordsuc  4600  dcextest  4618  peano2b  4652  opelxp  4694  opthprc  4715  relop  4817  issetid  4821  xpid11  4890  elres  4983  iss  4993  issref  5053  xpmlem  5091  sqxpeq0  5094  ssrnres  5113  dfrel2  5121  relrelss  5197  fn0  5380  funssxp  5430  f00  5452  f0bi  5453  dffo2  5487  ffoss  5539  f1o00  5542  fo00  5543  fv3  5584  dff2  5709  dffo4  5713  dffo5  5714  fmpt  5715  ffnfv  5723  fsn  5737  fsn2  5739  isores1  5864  ssoprab2b  5983  eqfnov2  6034  cnvoprab  6301  reldmtpos  6320  mapsn  6758  mapsncnv  6763  mptelixpg  6802  elixpsn  6803  ixpsnf1o  6804  en0  6863  en1  6867  dom0  6908  exmidpw  6978  exmidpweq  6979  pw1fin  6980  exmidpw2en  6982  undifdcss  6993  residfi  7015  fidcenum  7031  djuexb  7119  ctssdc  7188  exmidomni  7217  nninfwlpo  7254  exmidfodomr  7283  exmidontri  7322  exmidontri2or  7326  onntri3or  7328  onntri2or  7329  dftap2  7334  exmidmotap  7344  elni2  7398  ltbtwnnqq  7499  enq0ref  7517  elnp1st2nd  7560  elrealeu  7913  elreal2  7914  le2tri3i  8152  elnn0nn  9308  elnnnn0b  9310  elnnnn0c  9311  elnnz  9353  elnn0z  9356  elnnz1  9366  elz2  9414  eluz2b2  9694  elnn1uz2  9698  elpqb  9741  elioo4g  10026  eluzfz2b  10125  fzm  10130  elfz1end  10147  fzass4  10154  elfz1b  10182  fz01or  10203  nn0fz0  10211  fzolb  10246  fzom  10257  elfzo0  10275  fzo1fzo0n0  10276  elfzo0z  10277  elfzo1  10283  infssuzex  10340  wrdexb  10964  0wrd0  10978  rexanuz  11170  rexuz3  11172  sqrt0rlem  11185  fisum0diag  11623  fprod0diagfz  11810  isprm6  12340  oddpwdclemdc  12366  nnoddn2prmb  12456  4sqlem4  12586  4sqexercise1  12592  ennnfone  12667  ctinfom  12670  ctinf  12672  fnpr2ob  13042  dfgrp2  13229  dfgrp3m  13301  dfgrp3me  13302  isnsg3  13413  invghm  13535  dvdsrzring  14235  zrhval  14249  tgclb  14385  xmetunirn  14678  dich0  14972  elply2  15055  2sqlem2  15440  bj-nnsn  15463  bdeq  15553  bdop  15605  bdunexb  15650  bj-2inf  15668  bj-nn0suc  15694  nnnninfen  15752  exmidsbth  15755  trirec0  15775  redc0  15788  reap0  15789  cndcap  15790  neap0mkv  15800