Theorem impbid2 229

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 228	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
4	3	bicomd 226	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  biimt  363  bimsc1  857  biorf  949  pm4.72  964  19.38a  1867  19.38b  1868  ax13b  2059  19.3t  2243  cgsexg  3507  cgsex2g  3508  cgsex4g  3509  elab3gf  3652  elab3g  3653  abidnf  3674  reuan  3858  sscon34b  4265  r19.3rzv  4469  elsn2g  4635  eqoreldif  4656  difsn  4770  elpreqprb  4837  dfnfc2  4898  intmin4  4946  elpw2g  5304  ssrel  5770  ssrel2  5772  ssrelrel  5783  dmopab2rex  5908  releldmb  5937  relelrnb  5938  cnveqb  6196  dmsnopg  6215  relcnvtrg  6269  elsnxp  6293  onelssex  6411  ord0eln0  6418  f1ocnvb  6835  eqfnun  7033  ffvresb  7122  isof1oopb  7324  soisores  7326  riotaclb  7409  fnoprabg  7534  difex2  7759  dfwe2  7773  ordpwsuc  7811  ordunisuc2  7840  limsssuc  7846  dfom2  7864  relcnvexb  7923  dfsmo2  8334  ord1eln01  8481  ord2eln012  8482  omord  8553  nneob  8642  fsetcdmex  8860  pw2f1olem  9069  pwssfi  9161  sucdom  9204  1sdom  9215  fundmfibi  9293  f1dmvrnfibi  9298  fieq0  9381  hartogslem1  9504  rankr1ag  9774  rankeq0b  9832  fidomtri  9979  fidomtri2  9980  pr2ne  9989  isfin2-2  10303  enfin2i  10305  isfin3-2  10351  isf34lem6  10364  isfin1-2  10369  isfin1-3  10370  isfin7-2  10380  axgroth6  10813  ltsonq  10954  ltexnq  10960  znegclb  12631  rpneg  13050  nltpnft  13190  ngtmnft  13192  xrrebnd  13194  qextlt  13229  qextle  13230  iccneg  13499  fzsn  13594  fz1sbc  13628  fzdif1  13633  fzofzp1b  13794  ceilidz  13885  fleqceilz  13887  hashclb  14394  hashnncl  14402  hashfun  14474  reim0b  15170  rexanre  15398  rexuzre  15404  lo1resb  15615  o1resb  15617  dvdsext  16379  zob  16417  ncoprmgcdne1b  16708  pceq0  16931  pc11  16940  pcz  16941  ramtcl  17070  cshwsiun  17159  oduposb  18383  pospo  18399  cnvpsb  18635  tsrlemax  18642  issubg2  19208  issubg4  19212  eqg0subg  19267  ghmmhmb  19297  pmtrmvd  19526  mndodcong  19612  issubrng2  20643  issubrg2  20677  ring2idlqusb  21421  lpigen  21472  cyggic  21691  ip2eq  21772  maducoeval2  22766  eltg3  23088  bastop  23107  0top  23109  iscld3  23190  isclo2  23214  cnprest  23415  dfconn2  23545  comppfsc  23658  cmphaushmeo  23926  reghaus  23951  nrmhaus  23952  fbun  23966  fsubbas  23993  ufileu  24045  uffix  24047  txflf  24132  fclsrest  24150  flimfnfcls  24154  ptcmplem2  24179  tgpt1  24244  tgpt0  24245  isngp2  24723  nrgdomn  24797  nmhmcn  25248  iscmet3  25421  limcflf  26009  ply1nzb  26249  coe11  26379  dgreq0  26391  eldmgm  27152  sqf11  27269  sqff1o  27312  zabsle1  27426  lgsabs1  27466  lgsquadlem2  27511  madebday  28059  oldbday  28060  leslss  28068  oldfib  28536  z12negsclb  28640  bdayfin  28646  issubgr2  29563  uhgrissubgr  29566  usgrfilem  29618  uvtxnbgrb  29692  nbusgrvtxm1uvtx  29696  cusgrfilem3  29748  vdiscusgr  29822  wwlksn0s  30151  clwwlknon1loop  30390  clwwlknun  30404  nmobndi  31068  hmopadj2  32234  mdslle1i  32610  mdslle2i  32611  relfi  32888  ssrelf  32901  prodindf  33123  bnj1173  35335  r1filim  35440  revwlkb  35517  resconn  35637  cvmsval  35657  fmlafvel  35776  dmopab3rexdif  35796  elmrsubrn  35911  funsseq  36159  brcolinear  36450  outsideofeu  36522  lineunray  36538  nn0prpw  36723  ttcsnexbig  36921  bj-nfimexal  37120  bj-spvw  37146  bj-sngltag  37507  bj-elpwg  37576  bj-elsn0  37687  bj-opelid  37688  bj-opelidres  37693  bj-ideqg1  37696  bj-imdirval3  37716  bj-inftyexpiinj  37741  qdiff  37859  poimirlem26  38185  poimirlem27  38186  heicant  38194  cover2  38254  isbndx  38321  isbnd2  38322  equivbnd2  38331  prdsbnd2  38334  elghomlem2OLD  38425  isdrngo3  38498  riotaclbgBAD  39618  lssatle  39679  opcon3b  39860  cdlemk33N  41573  cdlemk34  41574  quadfac  42862  ioin9i8  42866  eu6w  43300  wepwsolem  43661  onsupmaxb  43858  rp-fakeimass  44130  iscard5  44154  cnvssb  44204  intimag  44274  ntrneiiso  44709  pm11.71  44999  pm14.122b  45025  pm14.123b  45028  iotavalb  45032  relwf  45568  elixpconstg  45699  eliuniin  45709  eliuniin2  45730  climreeq  46221  f1cof1b  47703  rexrsb  47726  afv0nbfvbi  47777  dfafn5b  47787  elfz2z  47941  zeo2ALTV  48325  fpprwpprb  48394  dfsclnbgr6  48512  nnlog2ge0lt1  49231  oppccatb  49679