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  1841  19.38b  1842  ax13b  2033  19.3t  2208  cgsexg  3485  cgsex2g  3486  cgsex4g  3487  cgsex4gOLD  3488  elab3gf  3639  elab3g  3640  abidnf  3660  reuan  3846  sscon34b  4256  r19.3rzv  4456  elsn2g  4621  eqoreldif  4642  difsn  4754  elpreqprb  4824  dfnfc2  4885  intmin4  4932  dfiin2g  4986  elpw2g  5278  ssrel  5732  ssrel2  5734  ssrelrel  5745  dmopab2rex  5866  releldmb  5895  relelrnb  5896  cnveqb  6154  dmsnopg  6171  relcnvtrg  6225  elsnxp  6249  onelssex  6366  ord0eln0  6373  f1ocnvb  6787  eqfnun  6982  ffvresb  7070  isof1oopb  7271  soisores  7273  riotaclb  7356  fnoprabg  7481  difex2  7705  dfwe2  7719  ordpwsuc  7757  ordunisuc2  7786  limsssuc  7792  dfom2  7810  relcnvexb  7868  dfsmo2  8279  ord1eln01  8423  ord2eln012  8424  omord  8495  nneob  8584  fsetcdmex  8800  pw2f1olem  9009  pwssfi  9101  sucdom  9144  1sdom  9155  fundmfibi  9236  f1dmvrnfibi  9241  fieq0  9324  hartogslem1  9447  rankr1ag  9714  rankeq0b  9772  fidomtri  9905  fidomtri2  9906  pr2ne  9915  isfin2-2  10229  enfin2i  10231  isfin3-2  10277  isf34lem6  10290  isfin1-2  10295  isfin1-3  10296  isfin7-2  10306  axgroth6  10739  ltsonq  10880  ltexnq  10886  znegclb  12528  rpneg  12939  nltpnft  13079  ngtmnft  13081  xrrebnd  13083  qextlt  13118  qextle  13119  iccneg  13388  fzsn  13482  fz1sbc  13516  fzdif1  13521  fzofzp1b  13681  ceilidz  13772  fleqceilz  13774  hashclb  14281  hashnncl  14289  hashfun  14360  reim0b  15042  rexanre  15270  rexuzre  15276  lo1resb  15487  o1resb  15489  dvdsext  16248  zob  16286  ncoprmgcdne1b  16577  pceq0  16799  pc11  16808  pcz  16809  ramtcl  16938  cshwsiun  17027  oduposb  18250  pospo  18266  cnvpsb  18502  tsrlemax  18509  issubg2  19071  issubg4  19075  eqg0subg  19125  ghmmhmb  19156  pmtrmvd  19385  mndodcong  19471  issubrng2  20491  issubrg2  20525  ring2idlqusb  21265  lpigen  21290  cyggic  21527  ip2eq  21608  maducoeval2  22584  eltg3  22906  bastop  22925  0top  22927  iscld3  23008  isclo2  23032  cnprest  23233  dfconn2  23363  comppfsc  23476  cmphaushmeo  23744  reghaus  23769  nrmhaus  23770  fbun  23784  fsubbas  23811  ufileu  23863  uffix  23865  txflf  23950  fclsrest  23968  flimfnfcls  23972  ptcmplem2  23997  tgpt1  24062  tgpt0  24063  isngp2  24541  nrgdomn  24615  nmhmcn  25076  iscmet3  25249  limcflf  25838  ply1nzb  26084  coe11  26214  dgreq0  26227  eldmgm  26988  sqf11  27105  sqff1o  27148  zabsle1  27263  lgsabs1  27303  lgsquadlem2  27348  madebday  27896  oldbday  27897  leslss  27905  oldfib  28373  z12negsclb  28477  bdayfin  28483  issubgr2  29345  uhgrissubgr  29348  usgrfilem  29400  uvtxnbgrb  29474  nbusgrvtxm1uvtx  29478  cusgrfilem3  29531  vdiscusgr  29605  wwlksn0s  29934  clwwlknon1loop  30173  clwwlknun  30187  nmobndi  30850  hmopadj2  32016  mdslle1i  32392  mdslle2i  32393  relfi  32677  ssrelf  32693  prodindf  32944  bnj1173  35158  r1filim  35260  revwlkb  35320  resconn  35440  cvmsval  35460  fmlafvel  35579  dmopab3rexdif  35599  elmrsubrn  35714  funsseq  35962  brcolinear  36253  outsideofeu  36325  lineunray  36341  nn0prpw  36517  bj-nfimexal  36826  bj-sngltag  37184  bj-elpwg  37253  bj-elsn0  37360  bj-opelid  37361  bj-opelidres  37366  bj-ideqg1  37369  bj-imdirval3  37389  bj-inftyexpiinj  37414  poimirlem26  37847  poimirlem27  37848  heicant  37856  cover2  37916  isbndx  37983  isbnd2  37984  equivbnd2  37993  prdsbnd2  37996  elghomlem2OLD  38087  isdrngo3  38160  riotaclbgBAD  39224  lssatle  39285  opcon3b  39466  cdlemk33N  41179  cdlemk34  41180  ioin9i8  42471  eu6w  42929  wepwsolem  43294  onsupmaxb  43491  rp-fakeimass  43763  iscard5  43787  cnvssb  43837  intimag  43907  ntrneiiso  44342  pm11.71  44648  pm14.122b  44674  pm14.123b  44677  iotavalb  44681  relwf  45218  elixpconstg  45343  eliuniin  45353  eliuniin2  45374  climreeq  45869  f1cof1b  47333  rexrsb  47356  afv0nbfvbi  47407  dfafn5b  47417  elfz2z  47571  zeo2ALTV  47927  fpprwpprb  47996  dfsclnbgr6  48114  nnlog2ge0lt1  48822  oppccatb  49271