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  3475  cgsex2g  3476  cgsex4g  3477  elab3gf  3628  elab3g  3629  abidnf  3649  reuan  3835  sscon34b  4245  r19.3rzv  4444  elsn2g  4609  eqoreldif  4630  difsn  4742  elpreqprb  4812  dfnfc2  4873  intmin4  4920  elpw2g  5271  ssrel  5733  ssrel2  5735  ssrelrel  5746  dmopab2rex  5867  releldmb  5896  relelrnb  5897  cnveqb  6155  dmsnopg  6172  relcnvtrg  6226  elsnxp  6250  onelssex  6367  ord0eln0  6374  f1ocnvb  6788  eqfnun  6984  ffvresb  7073  isof1oopb  7274  soisores  7276  riotaclb  7359  fnoprabg  7484  difex2  7708  dfwe2  7722  ordpwsuc  7760  ordunisuc2  7789  limsssuc  7795  dfom2  7813  relcnvexb  7871  dfsmo2  8281  ord1eln01  8425  ord2eln012  8426  omord  8497  nneob  8586  fsetcdmex  8804  pw2f1olem  9013  pwssfi  9105  sucdom  9148  1sdom  9159  fundmfibi  9240  f1dmvrnfibi  9245  fieq0  9328  hartogslem1  9451  rankr1ag  9720  rankeq0b  9778  fidomtri  9911  fidomtri2  9912  pr2ne  9921  isfin2-2  10235  enfin2i  10237  isfin3-2  10283  isf34lem6  10296  isfin1-2  10301  isfin1-3  10302  isfin7-2  10312  axgroth6  10745  ltsonq  10886  ltexnq  10892  znegclb  12558  rpneg  12970  nltpnft  13110  ngtmnft  13112  xrrebnd  13114  qextlt  13149  qextle  13150  iccneg  13419  fzsn  13514  fz1sbc  13548  fzdif1  13553  fzofzp1b  13714  ceilidz  13805  fleqceilz  13807  hashclb  14314  hashnncl  14322  hashfun  14393  reim0b  15075  rexanre  15303  rexuzre  15309  lo1resb  15520  o1resb  15522  dvdsext  16284  zob  16322  ncoprmgcdne1b  16613  pceq0  16836  pc11  16845  pcz  16846  ramtcl  16975  cshwsiun  17064  oduposb  18287  pospo  18303  cnvpsb  18539  tsrlemax  18546  issubg2  19111  issubg4  19115  eqg0subg  19165  ghmmhmb  19196  pmtrmvd  19425  mndodcong  19511  issubrng2  20529  issubrg2  20563  ring2idlqusb  21303  lpigen  21328  cyggic  21565  ip2eq  21646  maducoeval2  22618  eltg3  22940  bastop  22959  0top  22961  iscld3  23042  isclo2  23066  cnprest  23267  dfconn2  23397  comppfsc  23510  cmphaushmeo  23778  reghaus  23803  nrmhaus  23804  fbun  23818  fsubbas  23845  ufileu  23897  uffix  23899  txflf  23984  fclsrest  24002  flimfnfcls  24006  ptcmplem2  24031  tgpt1  24096  tgpt0  24097  isngp2  24575  nrgdomn  24649  nmhmcn  25100  iscmet3  25273  limcflf  25861  ply1nzb  26101  coe11  26231  dgreq0  26243  eldmgm  27002  sqf11  27119  sqff1o  27162  zabsle1  27276  lgsabs1  27316  lgsquadlem2  27361  madebday  27909  oldbday  27910  leslss  27918  oldfib  28386  z12negsclb  28490  bdayfin  28496  issubgr2  29358  uhgrissubgr  29361  usgrfilem  29413  uvtxnbgrb  29487  nbusgrvtxm1uvtx  29491  cusgrfilem3  29544  vdiscusgr  29618  wwlksn0s  29947  clwwlknon1loop  30186  clwwlknun  30200  nmobndi  30864  hmopadj2  32030  mdslle1i  32406  mdslle2i  32407  relfi  32690  ssrelf  32706  prodindf  32940  bnj1173  35163  r1filim  35266  revwlkb  35327  resconn  35447  cvmsval  35467  fmlafvel  35586  dmopab3rexdif  35606  elmrsubrn  35721  funsseq  35969  brcolinear  36260  outsideofeu  36332  lineunray  36348  nn0prpw  36524  ttcsnexbig  36722  bj-nfimexal  36922  bj-spvw  36948  bj-sngltag  37309  bj-elpwg  37378  bj-elsn0  37488  bj-opelid  37489  bj-opelidres  37494  bj-ideqg1  37497  bj-imdirval3  37517  bj-inftyexpiinj  37542  poimirlem26  37984  poimirlem27  37985  heicant  37993  cover2  38053  isbndx  38120  isbnd2  38121  equivbnd2  38130  prdsbnd2  38133  elghomlem2OLD  38224  isdrngo3  38297  riotaclbgBAD  39417  lssatle  39478  opcon3b  39659  cdlemk33N  41372  cdlemk34  41373  ioin9i8  42663  eu6w  43126  wepwsolem  43491  onsupmaxb  43688  rp-fakeimass  43960  iscard5  43984  cnvssb  44034  intimag  44104  ntrneiiso  44539  pm11.71  44845  pm14.122b  44871  pm14.123b  44874  iotavalb  44878  relwf  45415  elixpconstg  45540  eliuniin  45550  eliuniin2  45571  climreeq  46064  f1cof1b  47540  rexrsb  47563  afv0nbfvbi  47614  dfafn5b  47624  elfz2z  47778  zeo2ALTV  48162  fpprwpprb  48231  dfsclnbgr6  48349  nnlog2ge0lt1  49057  oppccatb  49506