Theorem impbid2 225

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 224	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
4	3	bicomd 222	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  biimt  360  bimsc1  840  biorf  933  pm4.72  946  19.38a  1843  19.38b  1844  ax13b  2036  19.3t  2197  sb3bOLD  2483  cgsexg  3464  cgsex2g  3465  cgsex4g  3466  cgsex4gOLD  3467  elab3gf  3608  elab3g  3609  abidnf  3633  reuan  3825  sscon34b  4225  elsn2g  4596  eqoreldif  4617  difsn  4728  elpreqprb  4795  dfnfc2  4860  intmin4  4905  dfiin2g  4958  elpw2g  5263  ssrel  5683  ssrel2  5685  ssrelrel  5695  dmopab2rex  5815  releldmb  5844  relelrnb  5845  cnveqb  6088  dmsnopg  6105  relcnvtrg  6159  elsnxp  6183  ord0eln0  6305  f1ocnvb  6713  ffvresb  6980  isof1oopb  7176  soisores  7178  riotaclb  7254  fnoprabg  7375  difex2  7588  dfwe2  7602  ordpwsuc  7637  ordunisuc2  7666  limsssuc  7672  dfom2  7689  relcnvexb  7747  dfsmo2  8149  omord  8361  nneob  8446  fsetcdmex  8609  pw2f1olem  8816  sucdom  8949  fundmfibi  9028  f1dmvrnfibi  9033  fieq0  9110  hartogslem1  9231  rankr1ag  9491  rankeq0b  9549  fidomtri  9682  fidomtri2  9683  isfin2-2  10006  enfin2i  10008  isfin3-2  10054  isf34lem6  10067  isfin1-2  10072  isfin1-3  10073  isfin7-2  10083  axgroth6  10515  ltsonq  10656  ltexnq  10662  znegclb  12287  rpneg  12691  nltpnft  12827  ngtmnft  12829  xrrebnd  12831  qextlt  12866  qextle  12867  iccneg  13133  fzsn  13227  fz1sbc  13261  fzofzp1b  13413  ceilidz  13500  fleqceilz  13502  hashclb  14001  hashnncl  14009  hashfun  14080  reim0b  14758  rexanre  14986  rexuzre  14992  lo1resb  15201  o1resb  15203  dvdsext  15958  zob  15996  ncoprmgcdne1b  16283  pceq0  16500  pc11  16509  pcz  16510  ramtcl  16639  cshwsiun  16729  oduposb  17962  pospo  17978  cnvpsb  18212  tsrlemax  18219  issubg2  18685  issubg4  18689  ghmmhmb  18760  pmtrmvd  18979  mndodcong  19065  issubrg2  19959  lpigen  20440  cyggic  20692  ip2eq  20770  maducoeval2  21697  eltg3  22020  bastop  22039  0top  22041  iscld3  22123  isclo2  22147  cnprest  22348  dfconn2  22478  comppfsc  22591  cmphaushmeo  22859  reghaus  22884  nrmhaus  22885  fbun  22899  fsubbas  22926  ufileu  22978  uffix  22980  txflf  23065  fclsrest  23083  flimfnfcls  23087  ptcmplem2  23112  tgpt1  23177  tgpt0  23178  isngp2  23659  nrgdomn  23741  nmhmcn  24189  iscmet3  24362  limcflf  24950  ply1nzb  25192  coe11  25319  dgreq0  25331  eldmgm  26076  sqf11  26193  sqff1o  26236  zabsle1  26349  lgsabs1  26389  lgsquadlem2  26434  issubgr2  27542  uhgrissubgr  27545  usgrfilem  27597  uvtxnbgrb  27671  nbusgrvtxm1uvtx  27675  cusgrfilem3  27727  vdiscusgr  27801  wwlksn0s  28127  clwwlknon1loop  28363  clwwlknun  28377  nmobndi  29038  hmopadj2  30204  mdslle1i  30580  mdslle2i  30581  relfi  30842  ssrelf  30856  prodindf  31891  bnj1173  32882  revwlkb  32987  resconn  33108  cvmsval  33128  fmlafvel  33247  dmopab3rexdif  33267  elmrsubrn  33382  onelssex  33563  funsseq  33648  madebday  34007  oldbday  34008  brcolinear  34288  outsideofeu  34360  lineunray  34376  nn0prpw  34439  bj-nfimexal  34734  bj-sngltag  35100  bj-elpwg  35152  bj-elsn0  35253  bj-opelid  35254  bj-opelidres  35259  bj-ideqg1  35262  bj-imdirval3  35282  bj-inftyexpiinj  35307  wl-ax11-lem2  35664  poimirlem26  35730  poimirlem27  35731  heicant  35739  cover2  35799  eqfnun  35807  isbndx  35867  isbnd2  35868  equivbnd2  35877  prdsbnd2  35880  elghomlem2OLD  35971  isdrngo3  36044  riotaclbgBAD  36895  lssatle  36956  opcon3b  37137  cdlemk33N  38850  cdlemk34  38851  ioin9i8  40101  wepwsolem  40783  rp-fakeimass  41017  iscard5  41039  cnvssb  41083  intimag  41153  ntrneiiso  41590  pm11.71  41904  pm14.122b  41930  pm14.123b  41933  iotavalb  41937  elixpconstg  42528  eliuniin  42538  eliuniin2  42558  climreeq  43044  f1cof1b  44456  rexrsb  44479  afv0nbfvbi  44530  dfafn5b  44540  elfz2z  44695  zeo2ALTV  45011  fpprwpprb  45080  nnlog2ge0lt1  45800