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  3495  cgsex2g  3496  cgsex4g  3497  cgsex4gOLD  3498  elab3gf  3654  elab3g  3655  abidnf  3676  reuan  3862  sscon34b  4270  elsn2g  4631  eqoreldif  4652  difsn  4765  elpreqprb  4835  dfnfc2  4896  intmin4  4944  dfiin2g  4999  elpw2g  5291  ssrel  5748  ssrelOLD  5749  ssrel2  5751  ssrelrel  5762  dmopab2rex  5884  releldmb  5913  relelrnb  5914  cnveqb  6172  dmsnopg  6189  relcnvtrg  6242  elsnxp  6267  onelssex  6384  ord0eln0  6391  f1ocnvb  6816  eqfnun  7012  ffvresb  7100  isof1oopb  7303  soisores  7305  riotaclb  7388  fnoprabg  7515  difex2  7739  dfwe2  7753  ordpwsuc  7793  ordunisuc2  7823  limsssuc  7829  dfom2  7847  relcnvexb  7905  dfsmo2  8319  ord1eln01  8463  ord2eln012  8464  omord  8535  nneob  8623  fsetcdmex  8839  pw2f1olem  9050  pwssfi  9147  sucdom  9189  sucdomOLD  9190  1sdom  9202  fundmfibi  9294  f1dmvrnfibi  9299  fieq0  9379  hartogslem1  9502  rankr1ag  9762  rankeq0b  9820  fidomtri  9953  fidomtri2  9954  pr2ne  9964  isfin2-2  10279  enfin2i  10281  isfin3-2  10327  isf34lem6  10340  isfin1-2  10345  isfin1-3  10346  isfin7-2  10356  axgroth6  10788  ltsonq  10929  ltexnq  10935  znegclb  12577  rpneg  12992  nltpnft  13131  ngtmnft  13133  xrrebnd  13135  qextlt  13170  qextle  13171  iccneg  13440  fzsn  13534  fz1sbc  13568  fzdif1  13573  fzofzp1b  13733  ceilidz  13821  fleqceilz  13823  hashclb  14330  hashnncl  14338  hashfun  14409  reim0b  15092  rexanre  15320  rexuzre  15326  lo1resb  15537  o1resb  15539  dvdsext  16298  zob  16336  ncoprmgcdne1b  16627  pceq0  16849  pc11  16858  pcz  16859  ramtcl  16988  cshwsiun  17077  oduposb  18295  pospo  18311  cnvpsb  18545  tsrlemax  18552  issubg2  19080  issubg4  19084  eqg0subg  19135  ghmmhmb  19166  pmtrmvd  19393  mndodcong  19479  issubrng2  20474  issubrg2  20508  ring2idlqusb  21227  lpigen  21252  cyggic  21489  ip2eq  21569  maducoeval2  22534  eltg3  22856  bastop  22875  0top  22877  iscld3  22958  isclo2  22982  cnprest  23183  dfconn2  23313  comppfsc  23426  cmphaushmeo  23694  reghaus  23719  nrmhaus  23720  fbun  23734  fsubbas  23761  ufileu  23813  uffix  23815  txflf  23900  fclsrest  23918  flimfnfcls  23922  ptcmplem2  23947  tgpt1  24012  tgpt0  24013  isngp2  24492  nrgdomn  24566  nmhmcn  25027  iscmet3  25200  limcflf  25789  ply1nzb  26035  coe11  26165  dgreq0  26178  eldmgm  26939  sqf11  27056  sqff1o  27099  zabsle1  27214  lgsabs1  27254  lgsquadlem2  27299  madebday  27818  oldbday  27819  slelss  27827  zs12negsclb  28348  issubgr2  29206  uhgrissubgr  29209  usgrfilem  29261  uvtxnbgrb  29335  nbusgrvtxm1uvtx  29339  cusgrfilem3  29392  vdiscusgr  29466  wwlksn0s  29798  clwwlknon1loop  30034  clwwlknun  30048  nmobndi  30711  hmopadj2  31877  mdslle1i  32253  mdslle2i  32254  relfi  32538  ssrelf  32550  prodindf  32793  bnj1173  34999  revwlkb  35120  resconn  35240  cvmsval  35260  fmlafvel  35379  dmopab3rexdif  35399  elmrsubrn  35514  funsseq  35762  brcolinear  36054  outsideofeu  36126  lineunray  36142  nn0prpw  36318  bj-nfimexal  36621  bj-sngltag  36978  bj-elpwg  37047  bj-elsn0  37150  bj-opelid  37151  bj-opelidres  37156  bj-ideqg1  37159  bj-imdirval3  37179  bj-inftyexpiinj  37204  wl-ax11-lem2  37581  poimirlem26  37647  poimirlem27  37648  heicant  37656  cover2  37716  isbndx  37783  isbnd2  37784  equivbnd2  37793  prdsbnd2  37796  elghomlem2OLD  37887  isdrngo3  37960  riotaclbgBAD  38954  lssatle  39015  opcon3b  39196  cdlemk33N  40910  cdlemk34  40911  ioin9i8  42202  eu6w  42671  wepwsolem  43038  onsupmaxb  43235  rp-fakeimass  43508  iscard5  43532  cnvssb  43582  intimag  43652  ntrneiiso  44087  pm11.71  44393  pm14.122b  44419  pm14.123b  44422  iotavalb  44426  relwf  44964  elixpconstg  45090  eliuniin  45100  eliuniin2  45121  climreeq  45618  f1cof1b  47082  rexrsb  47105  afv0nbfvbi  47156  dfafn5b  47166  elfz2z  47320  zeo2ALTV  47676  fpprwpprb  47745  dfsclnbgr6  47862  nnlog2ge0lt1  48559  oppccatb  49009