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  1840  19.38b  1841  ax13b  2031  19.3t  2201  cgsexg  3526  cgsex2g  3527  cgsex4g  3528  cgsex4gOLD  3529  elab3gf  3684  elab3g  3685  abidnf  3708  reuan  3896  sscon34b  4304  elsn2g  4664  eqoreldif  4685  difsn  4798  elpreqprb  4868  dfnfc2  4929  intmin4  4977  dfiin2g  5032  elpw2g  5333  ssrel  5792  ssrelOLD  5793  ssrel2  5795  ssrelrel  5806  dmopab2rex  5928  releldmb  5957  relelrnb  5958  cnveqb  6216  dmsnopg  6233  relcnvtrg  6286  elsnxp  6311  onelssex  6432  ord0eln0  6439  f1ocnvb  6861  eqfnun  7057  ffvresb  7145  isof1oopb  7345  soisores  7347  riotaclb  7429  fnoprabg  7556  difex2  7780  dfwe2  7794  ordpwsuc  7835  ordunisuc2  7865  limsssuc  7871  dfom2  7889  relcnvexb  7948  dfsmo2  8387  ord1eln01  8534  ord2eln012  8535  omord  8606  nneob  8694  fsetcdmex  8903  pw2f1olem  9116  pwssfi  9217  sucdom  9271  sucdomOLD  9272  1sdom  9284  fundmfibi  9376  f1dmvrnfibi  9381  fieq0  9461  hartogslem1  9582  rankr1ag  9842  rankeq0b  9900  fidomtri  10033  fidomtri2  10034  pr2ne  10044  isfin2-2  10359  enfin2i  10361  isfin3-2  10407  isf34lem6  10420  isfin1-2  10425  isfin1-3  10426  isfin7-2  10436  axgroth6  10868  ltsonq  11009  ltexnq  11015  znegclb  12654  rpneg  13067  nltpnft  13206  ngtmnft  13208  xrrebnd  13210  qextlt  13245  qextle  13246  iccneg  13512  fzsn  13606  fz1sbc  13640  fzdif1  13645  fzofzp1b  13804  ceilidz  13892  fleqceilz  13894  hashclb  14397  hashnncl  14405  hashfun  14476  reim0b  15158  rexanre  15385  rexuzre  15391  lo1resb  15600  o1resb  15602  dvdsext  16358  zob  16396  ncoprmgcdne1b  16687  pceq0  16909  pc11  16918  pcz  16919  ramtcl  17048  cshwsiun  17137  oduposb  18374  pospo  18390  cnvpsb  18624  tsrlemax  18631  issubg2  19159  issubg4  19163  eqg0subg  19214  ghmmhmb  19245  pmtrmvd  19474  mndodcong  19560  issubrng2  20558  issubrg2  20592  ring2idlqusb  21320  lpigen  21345  cyggic  21591  ip2eq  21671  maducoeval2  22646  eltg3  22969  bastop  22988  0top  22990  iscld3  23072  isclo2  23096  cnprest  23297  dfconn2  23427  comppfsc  23540  cmphaushmeo  23808  reghaus  23833  nrmhaus  23834  fbun  23848  fsubbas  23875  ufileu  23927  uffix  23929  txflf  24014  fclsrest  24032  flimfnfcls  24036  ptcmplem2  24061  tgpt1  24126  tgpt0  24127  isngp2  24610  nrgdomn  24692  nmhmcn  25153  iscmet3  25327  limcflf  25916  ply1nzb  26162  coe11  26292  dgreq0  26305  eldmgm  27065  sqf11  27182  sqff1o  27225  zabsle1  27340  lgsabs1  27380  lgsquadlem2  27425  madebday  27938  oldbday  27939  slelss  27946  issubgr2  29289  uhgrissubgr  29292  usgrfilem  29344  uvtxnbgrb  29418  nbusgrvtxm1uvtx  29422  cusgrfilem3  29475  vdiscusgr  29549  wwlksn0s  29881  clwwlknon1loop  30117  clwwlknun  30131  nmobndi  30794  hmopadj2  31960  mdslle1i  32336  mdslle2i  32337  relfi  32615  ssrelf  32627  prodindf  32848  bnj1173  35016  revwlkb  35131  resconn  35251  cvmsval  35271  fmlafvel  35390  dmopab3rexdif  35410  elmrsubrn  35525  funsseq  35768  brcolinear  36060  outsideofeu  36132  lineunray  36148  nn0prpw  36324  bj-nfimexal  36627  bj-sngltag  36984  bj-elpwg  37053  bj-elsn0  37156  bj-opelid  37157  bj-opelidres  37162  bj-ideqg1  37165  bj-imdirval3  37185  bj-inftyexpiinj  37210  wl-ax11-lem2  37587  poimirlem26  37653  poimirlem27  37654  heicant  37662  cover2  37722  isbndx  37789  isbnd2  37790  equivbnd2  37799  prdsbnd2  37802  elghomlem2OLD  37893  isdrngo3  37966  riotaclbgBAD  38955  lssatle  39016  opcon3b  39197  cdlemk33N  40911  cdlemk34  40912  ioin9i8  42246  eu6w  42686  wepwsolem  43054  onsupmaxb  43251  rp-fakeimass  43525  iscard5  43549  cnvssb  43599  intimag  43669  ntrneiiso  44104  pm11.71  44416  pm14.122b  44442  pm14.123b  44445  iotavalb  44449  relwf  44984  elixpconstg  45094  eliuniin  45104  eliuniin2  45125  climreeq  45628  f1cof1b  47089  rexrsb  47112  afv0nbfvbi  47163  dfafn5b  47173  elfz2z  47327  zeo2ALTV  47658  fpprwpprb  47727  dfsclnbgr6  47844  nnlog2ge0lt1  48487