Theorem impbid2 226

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	⊢ (𝜓 → 𝜒)
impbid2.2	⊢ (𝜑 → (𝜒 → 𝜓))

Assertion

Ref	Expression
impbid2	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem impbid2

Step	Hyp	Ref	Expression
1		impbid2.2	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
2		impbid2.1	. . 3 ⊢ (𝜓 → 𝜒)
3	1, 2	impbid1 225	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
4	3	bicomd 223	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  biimt  360  bimsc1  844  biorf  936  pm4.72  951  19.38a  1836  19.38b  1837  ax13b  2028  19.3t  2198  cgsexg  3523  cgsex2g  3524  cgsex4g  3525  cgsex4gOLD  3526  elab3gf  3686  elab3g  3687  abidnf  3710  reuan  3904  sscon34b  4309  elsn2g  4668  eqoreldif  4689  difsn  4802  elpreqprb  4872  dfnfc2  4933  intmin4  4981  dfiin2g  5036  elpw2g  5338  ssrel  5794  ssrelOLD  5795  ssrel2  5797  ssrelrel  5808  dmopab2rex  5930  releldmb  5959  relelrnb  5960  cnveqb  6217  dmsnopg  6234  relcnvtrg  6287  elsnxp  6312  onelssex  6433  ord0eln0  6440  f1ocnvb  6861  eqfnun  7056  ffvresb  7144  isof1oopb  7344  soisores  7346  riotaclb  7428  fnoprabg  7555  difex2  7778  dfwe2  7792  ordpwsuc  7834  ordunisuc2  7864  limsssuc  7870  dfom2  7888  relcnvexb  7948  dfsmo2  8385  ord1eln01  8532  ord2eln012  8533  omord  8604  nneob  8692  fsetcdmex  8901  pw2f1olem  9114  sucdom  9268  sucdomOLD  9269  1sdom  9281  fundmfibi  9373  f1dmvrnfibi  9378  fieq0  9458  hartogslem1  9579  rankr1ag  9839  rankeq0b  9897  fidomtri  10030  fidomtri2  10031  pr2ne  10041  isfin2-2  10356  enfin2i  10358  isfin3-2  10404  isf34lem6  10417  isfin1-2  10422  isfin1-3  10423  isfin7-2  10433  axgroth6  10865  ltsonq  11006  ltexnq  11012  znegclb  12651  rpneg  13064  nltpnft  13202  ngtmnft  13204  xrrebnd  13206  qextlt  13241  qextle  13242  iccneg  13508  fzsn  13602  fz1sbc  13636  fzdif1  13641  fzofzp1b  13800  ceilidz  13888  fleqceilz  13890  hashclb  14393  hashnncl  14401  hashfun  14472  reim0b  15154  rexanre  15381  rexuzre  15387  lo1resb  15596  o1resb  15598  dvdsext  16354  zob  16392  ncoprmgcdne1b  16683  pceq0  16904  pc11  16913  pcz  16914  ramtcl  17043  cshwsiun  17133  oduposb  18386  pospo  18402  cnvpsb  18636  tsrlemax  18643  issubg2  19171  issubg4  19175  eqg0subg  19226  ghmmhmb  19257  pmtrmvd  19488  mndodcong  19574  issubrng2  20574  issubrg2  20608  ring2idlqusb  21337  lpigen  21362  cyggic  21608  ip2eq  21688  maducoeval2  22661  eltg3  22984  bastop  23003  0top  23005  iscld3  23087  isclo2  23111  cnprest  23312  dfconn2  23442  comppfsc  23555  cmphaushmeo  23823  reghaus  23848  nrmhaus  23849  fbun  23863  fsubbas  23890  ufileu  23942  uffix  23944  txflf  24029  fclsrest  24047  flimfnfcls  24051  ptcmplem2  24076  tgpt1  24141  tgpt0  24142  isngp2  24625  nrgdomn  24707  nmhmcn  25166  iscmet3  25340  limcflf  25930  ply1nzb  26176  coe11  26306  dgreq0  26319  eldmgm  27079  sqf11  27196  sqff1o  27239  zabsle1  27354  lgsabs1  27394  lgsquadlem2  27439  madebday  27952  oldbday  27953  slelss  27960  issubgr2  29303  uhgrissubgr  29306  usgrfilem  29358  uvtxnbgrb  29432  nbusgrvtxm1uvtx  29436  cusgrfilem3  29489  vdiscusgr  29563  wwlksn0s  29890  clwwlknon1loop  30126  clwwlknun  30140  nmobndi  30803  hmopadj2  31969  mdslle1i  32345  mdslle2i  32346  relfi  32621  ssrelf  32634  prodindf  34003  bnj1173  34994  revwlkb  35109  resconn  35230  cvmsval  35250  fmlafvel  35369  dmopab3rexdif  35389  elmrsubrn  35504  funsseq  35748  brcolinear  36040  outsideofeu  36112  lineunray  36128  nn0prpw  36305  bj-nfimexal  36608  bj-sngltag  36965  bj-elpwg  37034  bj-elsn0  37137  bj-opelid  37138  bj-opelidres  37143  bj-ideqg1  37146  bj-imdirval3  37166  bj-inftyexpiinj  37191  wl-ax11-lem2  37566  poimirlem26  37632  poimirlem27  37633  heicant  37641  cover2  37701  isbndx  37768  isbnd2  37769  equivbnd2  37778  prdsbnd2  37781  elghomlem2OLD  37872  isdrngo3  37945  riotaclbgBAD  38935  lssatle  38996  opcon3b  39177  cdlemk33N  40891  cdlemk34  40892  ioin9i8  42225  eu6w  42662  wepwsolem  43030  onsupmaxb  43227  rp-fakeimass  43501  iscard5  43525  cnvssb  43575  intimag  43645  ntrneiiso  44080  pm11.71  44392  pm14.122b  44418  pm14.123b  44421  iotavalb  44425  relwf  44941  elixpconstg  45028  eliuniin  45038  eliuniin2  45059  climreeq  45568  f1cof1b  47026  rexrsb  47049  afv0nbfvbi  47100  dfafn5b  47110  elfz2z  47264  zeo2ALTV  47595  fpprwpprb  47664  dfsclnbgr6  47781  nnlog2ge0lt1  48415