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  845  biorf  937  pm4.72  952  19.38a  1842  19.38b  1843  ax13b  2034  19.3t  2209  cgsexg  3474  cgsex2g  3475  cgsex4g  3476  elab3gf  3627  elab3g  3628  abidnf  3648  reuan  3834  sscon34b  4244  r19.3rzv  4443  elsn2g  4608  eqoreldif  4629  difsn  4743  elpreqprb  4811  dfnfc2  4872  intmin4  4919  elpw2g  5274  ssrel  5739  ssrel2  5741  ssrelrel  5752  dmopab2rex  5872  releldmb  5901  relelrnb  5902  cnveqb  6160  dmsnopg  6177  relcnvtrg  6231  elsnxp  6255  onelssex  6372  ord0eln0  6379  f1ocnvb  6793  eqfnun  6989  ffvresb  7078  isof1oopb  7280  soisores  7282  riotaclb  7365  fnoprabg  7490  difex2  7714  dfwe2  7728  ordpwsuc  7766  ordunisuc2  7795  limsssuc  7801  dfom2  7819  relcnvexb  7877  dfsmo2  8287  ord1eln01  8431  ord2eln012  8432  omord  8503  nneob  8592  fsetcdmex  8810  pw2f1olem  9019  pwssfi  9111  sucdom  9154  1sdom  9165  fundmfibi  9246  f1dmvrnfibi  9251  fieq0  9334  hartogslem1  9457  rankr1ag  9726  rankeq0b  9784  fidomtri  9917  fidomtri2  9918  pr2ne  9927  isfin2-2  10241  enfin2i  10243  isfin3-2  10289  isf34lem6  10302  isfin1-2  10307  isfin1-3  10308  isfin7-2  10318  axgroth6  10751  ltsonq  10892  ltexnq  10898  znegclb  12564  rpneg  12976  nltpnft  13116  ngtmnft  13118  xrrebnd  13120  qextlt  13155  qextle  13156  iccneg  13425  fzsn  13520  fz1sbc  13554  fzdif1  13559  fzofzp1b  13720  ceilidz  13811  fleqceilz  13813  hashclb  14320  hashnncl  14328  hashfun  14399  reim0b  15081  rexanre  15309  rexuzre  15315  lo1resb  15526  o1resb  15528  dvdsext  16290  zob  16328  ncoprmgcdne1b  16619  pceq0  16842  pc11  16851  pcz  16852  ramtcl  16981  cshwsiun  17070  oduposb  18293  pospo  18309  cnvpsb  18545  tsrlemax  18552  issubg2  19117  issubg4  19121  eqg0subg  19171  ghmmhmb  19202  pmtrmvd  19431  mndodcong  19517  issubrng2  20535  issubrg2  20569  ring2idlqusb  21308  lpigen  21333  cyggic  21552  ip2eq  21633  maducoeval2  22605  eltg3  22927  bastop  22946  0top  22948  iscld3  23029  isclo2  23053  cnprest  23254  dfconn2  23384  comppfsc  23497  cmphaushmeo  23765  reghaus  23790  nrmhaus  23791  fbun  23805  fsubbas  23832  ufileu  23884  uffix  23886  txflf  23971  fclsrest  23989  flimfnfcls  23993  ptcmplem2  24018  tgpt1  24083  tgpt0  24084  isngp2  24562  nrgdomn  24636  nmhmcn  25087  iscmet3  25260  limcflf  25848  ply1nzb  26088  coe11  26218  dgreq0  26230  eldmgm  26985  sqf11  27102  sqff1o  27145  zabsle1  27259  lgsabs1  27299  lgsquadlem2  27344  madebday  27892  oldbday  27893  leslss  27901  oldfib  28369  z12negsclb  28473  bdayfin  28479  issubgr2  29341  uhgrissubgr  29344  usgrfilem  29396  uvtxnbgrb  29470  nbusgrvtxm1uvtx  29474  cusgrfilem3  29526  vdiscusgr  29600  wwlksn0s  29929  clwwlknon1loop  30168  clwwlknun  30182  nmobndi  30846  hmopadj2  32012  mdslle1i  32388  mdslle2i  32389  relfi  32672  ssrelf  32688  prodindf  32922  bnj1173  35144  r1filim  35247  revwlkb  35308  resconn  35428  cvmsval  35448  fmlafvel  35567  dmopab3rexdif  35587  elmrsubrn  35702  funsseq  35950  brcolinear  36241  outsideofeu  36313  lineunray  36329  nn0prpw  36505  ttcsnexbig  36703  bj-nfimexal  36903  bj-spvw  36929  bj-sngltag  37290  bj-elpwg  37359  bj-elsn0  37469  bj-opelid  37470  bj-opelidres  37475  bj-ideqg1  37478  bj-imdirval3  37498  bj-inftyexpiinj  37523  qdiff  37641  poimirlem26  37967  poimirlem27  37968  heicant  37976  cover2  38036  isbndx  38103  isbnd2  38104  equivbnd2  38113  prdsbnd2  38116  elghomlem2OLD  38207  isdrngo3  38280  riotaclbgBAD  39400  lssatle  39461  opcon3b  39642  cdlemk33N  41355  cdlemk34  41356  ioin9i8  42646  eu6w  43109  wepwsolem  43470  onsupmaxb  43667  rp-fakeimass  43939  iscard5  43963  cnvssb  44013  intimag  44083  ntrneiiso  44518  pm11.71  44824  pm14.122b  44850  pm14.123b  44853  iotavalb  44857  relwf  45394  elixpconstg  45519  eliuniin  45529  eliuniin2  45550  climreeq  46043  f1cof1b  47525  rexrsb  47548  afv0nbfvbi  47599  dfafn5b  47609  elfz2z  47763  zeo2ALTV  48147  fpprwpprb  48216  dfsclnbgr6  48334  nnlog2ge0lt1  49042  oppccatb  49491