Theorem impbid2 216

Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) (Proof shortened by Wolf Lammen, 27-Sep-2013.)

Hypotheses

Ref	Expression
impbid2.1	|- ( ps -> ch )
impbid2.2	|- ( ph -> ( ch -> ps ) )

Assertion

Ref	Expression
impbid2	|- ( ph -> ( ps <-> ch ) )

Proof of Theorem impbid2

Step	Hyp	Ref	Expression
1		impbid2.2	. . 3 |- ( ph -> ( ch -> ps ) )
2		impbid2.1	. . 3 |- ( ps -> ch )
3	1, 2	impbid1 215	. 2 |- ( ph -> ( ch <-> ps ) )
4	3	bicomd 213	1 |- ( ph -> ( ps <-> ch ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  biimt  350  biorf  420  biorfiOLD  423  pm4.72  920  biort  938  bimsc1  980  19.38a  1767  19.38b  1768  ax13b  1964  cgsexg  3238  cgsex2g  3239  cgsex4g  3240  elab3gf  3356  abidnf  3375  elsn2g  4210  eqoreldif  4225  difsn  4328  eqsnOLD  4362  prel12  4383  elpreqprb  4397  dfnfc2  4454  dfnfc2OLD  4455  intmin4  4506  dfiin2g  4553  elpw2g  4827  ssrel  5207  ssrelOLD  5208  ssrel2  5210  ssrelrel  5220  releldmb  5360  relelrnb  5361  cnveqb  5590  dmsnopg  5606  relcnvtr  5655  elsnxp  5677  ord0eln0  5779  f1ocnvb  6150  ffvresb  6394  isof1oopb  6575  soisores  6577  riotaclb  6649  fnoprabg  6761  difex2  6969  dfwe2  6981  ordpwsuc  7015  ordunisuc2  7044  limsssuc  7050  dfom2  7067  relcnvexb  7114  dfsmo2  7444  omord  7648  nneob  7732  pw2f1olem  8064  sucdom  8157  fundmfibi  8245  f1dmvrnfibi  8250  fieq0  8327  hartogslem1  8447  rankr1ag  8665  rankeq0b  8723  fidomtri  8819  fidomtri2  8820  isfin2-2  9141  enfin2i  9143  isfin3-2  9189  isf34lem6  9202  isfin1-2  9207  isfin1-3  9208  isfin7-2  9218  axgroth6  9650  ltsonq  9791  ltexnq  9797  znegclb  11414  rpneg  11863  nltpnft  11995  ngtmnft  11997  xrrebnd  11999  qextlt  12034  qextle  12035  iccneg  12293  fzsn  12383  fz1sbc  12416  fzofzp1b  12566  ceilidz  12651  fleqceilz  12653  hashclb  13149  hashnncl  13157  hashfun  13224  reim0b  13859  rexanre  14086  rexuzre  14092  lo1resb  14295  o1resb  14297  dvdsext  15043  zob  15083  ncoprmgcdne1b  15363  pceq0  15575  pc11  15584  pcz  15585  ramtcl  15714  cshwsiun  15806  pospo  16973  oduposb  17136  cnvpsb  17213  tsrlemax  17220  issubg2  17609  issubg4  17613  ghmmhmb  17671  pmtrmvd  17876  mndodcong  17961  issubrg2  18800  lpigen  19256  cyggic  19921  ip2eq  19998  maducoeval2  20446  eltg3  20766  bastop  20785  0top  20787  iscld3  20868  isclo2  20892  cnprest  21093  dfconn2  21222  comppfsc  21335  cmphaushmeo  21603  reghaus  21628  nrmhaus  21629  fbun  21644  fsubbas  21671  ufileu  21723  uffix  21725  txflf  21810  fclsrest  21828  flimfnfcls  21832  ptcmplem2  21857  tgpt1  21921  tgpt0  21922  isngp2  22401  nrgdomn  22475  nmhmcn  22920  iscmet3  23091  limcflf  23645  ply1nzb  23882  coe11  24009  dgreq0  24021  eldmgm  24748  sqf11  24865  sqff1o  24908  zabsle1  25021  lgsabs1  25061  lgsquadlem2  25106  issubgr2  26164  uhgrissubgr  26167  usgrfilem  26219  uvtxnbgrb  26302  cusgrfilem3  26353  vdiscusgr  26427  wwlksn0s  26746  nmobndi  27630  hmopadj2  28800  mdslle1i  29176  mdslle2i  29177  relfi  29415  ssrelf  29425  prodindf  30085  bnj1173  31070  resconn  31228  cvmsval  31248  elmrsubrn  31417  funsseq  31666  brcolinear  32166  outsideofeu  32238  lineunray  32254  nn0prpw  32318  bj-19.3t  32689  bj-sb3b  32804  bj-sngltag  32971  bj-elid2  33086  bj-inftyexpiinj  33096  wl-sb5nae  33340  wl-ax11-lem2  33363  poimirlem26  33435  poimirlem27  33436  heicant  33444  cover2  33508  eqfnun  33516  isbndx  33581  isbnd2  33582  equivbnd2  33591  prdsbnd2  33594  elghomlem2OLD  33685  isdrngo3  33758  riotaclbgBAD  34240  lssatle  34302  opcon3b  34483  cdlemk33N  36197  cdlemk34  36198  wepwsolem  37612  rp-fakeimass  37857  cnvssb  37892  intimag  37948  sscon34b  38317  ntrneiiso  38389  pm11.71  38597  pm14.122b  38624  pm14.123b  38627  iotavalb  38631  eliuniin  39279  eliuniin2  39303  climreeq  39845  rexrsb  41169  reuan  41180  afv0nbfvbi  41231  dfafn5b  41241  elfz2z  41325  zeo2ALTV  41582  nnlog2ge0lt1  42360