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  1840  19.38b  1841  ax13b  2032  19.3t  2202  cgsexg  3489  cgsex2g  3490  cgsex4g  3491  cgsex4gOLD  3492  elab3gf  3648  elab3g  3649  abidnf  3670  reuan  3856  sscon34b  4263  elsn2g  4624  eqoreldif  4645  difsn  4758  elpreqprb  4828  dfnfc2  4889  intmin4  4937  dfiin2g  4991  elpw2g  5283  ssrel  5737  ssrel2  5739  ssrelrel  5750  dmopab2rex  5871  releldmb  5899  relelrnb  5900  cnveqb  6157  dmsnopg  6174  relcnvtrg  6227  elsnxp  6252  onelssex  6369  ord0eln0  6376  f1ocnvb  6795  eqfnun  6991  ffvresb  7079  isof1oopb  7282  soisores  7284  riotaclb  7367  fnoprabg  7492  difex2  7716  dfwe2  7730  ordpwsuc  7770  ordunisuc2  7800  limsssuc  7806  dfom2  7824  relcnvexb  7882  dfsmo2  8293  ord1eln01  8437  ord2eln012  8438  omord  8509  nneob  8597  fsetcdmex  8813  pw2f1olem  9022  pwssfi  9118  sucdom  9160  1sdom  9171  fundmfibi  9263  f1dmvrnfibi  9268  fieq0  9348  hartogslem1  9471  rankr1ag  9731  rankeq0b  9789  fidomtri  9922  fidomtri2  9923  pr2ne  9933  isfin2-2  10248  enfin2i  10250  isfin3-2  10296  isf34lem6  10309  isfin1-2  10314  isfin1-3  10315  isfin7-2  10325  axgroth6  10757  ltsonq  10898  ltexnq  10904  znegclb  12546  rpneg  12961  nltpnft  13100  ngtmnft  13102  xrrebnd  13104  qextlt  13139  qextle  13140  iccneg  13409  fzsn  13503  fz1sbc  13537  fzdif1  13542  fzofzp1b  13702  ceilidz  13790  fleqceilz  13792  hashclb  14299  hashnncl  14307  hashfun  14378  reim0b  15061  rexanre  15289  rexuzre  15295  lo1resb  15506  o1resb  15508  dvdsext  16267  zob  16305  ncoprmgcdne1b  16596  pceq0  16818  pc11  16827  pcz  16828  ramtcl  16957  cshwsiun  17046  oduposb  18264  pospo  18280  cnvpsb  18514  tsrlemax  18521  issubg2  19049  issubg4  19053  eqg0subg  19104  ghmmhmb  19135  pmtrmvd  19362  mndodcong  19448  issubrng2  20443  issubrg2  20477  ring2idlqusb  21196  lpigen  21221  cyggic  21458  ip2eq  21538  maducoeval2  22503  eltg3  22825  bastop  22844  0top  22846  iscld3  22927  isclo2  22951  cnprest  23152  dfconn2  23282  comppfsc  23395  cmphaushmeo  23663  reghaus  23688  nrmhaus  23689  fbun  23703  fsubbas  23730  ufileu  23782  uffix  23784  txflf  23869  fclsrest  23887  flimfnfcls  23891  ptcmplem2  23916  tgpt1  23981  tgpt0  23982  isngp2  24461  nrgdomn  24535  nmhmcn  24996  iscmet3  25169  limcflf  25758  ply1nzb  26004  coe11  26134  dgreq0  26147  eldmgm  26908  sqf11  27025  sqff1o  27068  zabsle1  27183  lgsabs1  27223  lgsquadlem2  27268  madebday  27787  oldbday  27788  slelss  27796  zs12negsclb  28317  issubgr2  29175  uhgrissubgr  29178  usgrfilem  29230  uvtxnbgrb  29304  nbusgrvtxm1uvtx  29308  cusgrfilem3  29361  vdiscusgr  29435  wwlksn0s  29764  clwwlknon1loop  30000  clwwlknun  30014  nmobndi  30677  hmopadj2  31843  mdslle1i  32219  mdslle2i  32220  relfi  32504  ssrelf  32516  prodindf  32759  bnj1173  34965  revwlkb  35086  resconn  35206  cvmsval  35226  fmlafvel  35345  dmopab3rexdif  35365  elmrsubrn  35480  funsseq  35728  brcolinear  36020  outsideofeu  36092  lineunray  36108  nn0prpw  36284  bj-nfimexal  36587  bj-sngltag  36944  bj-elpwg  37013  bj-elsn0  37116  bj-opelid  37117  bj-opelidres  37122  bj-ideqg1  37125  bj-imdirval3  37145  bj-inftyexpiinj  37170  wl-ax11-lem2  37547  poimirlem26  37613  poimirlem27  37614  heicant  37622  cover2  37682  isbndx  37749  isbnd2  37750  equivbnd2  37759  prdsbnd2  37762  elghomlem2OLD  37853  isdrngo3  37926  riotaclbgBAD  38920  lssatle  38981  opcon3b  39162  cdlemk33N  40876  cdlemk34  40877  ioin9i8  42168  eu6w  42637  wepwsolem  43004  onsupmaxb  43201  rp-fakeimass  43474  iscard5  43498  cnvssb  43548  intimag  43618  ntrneiiso  44053  pm11.71  44359  pm14.122b  44385  pm14.123b  44388  iotavalb  44392  relwf  44930  elixpconstg  45056  eliuniin  45066  eliuniin2  45087  climreeq  45584  f1cof1b  47051  rexrsb  47074  afv0nbfvbi  47125  dfafn5b  47135  elfz2z  47289  zeo2ALTV  47645  fpprwpprb  47714  dfsclnbgr6  47831  nnlog2ge0lt1  48528  oppccatb  48978