Theorem impbid2 229

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  biimt  364  bimsc1  844  biorf  937  pm4.72  950  19.38a  1847  19.38b  1848  ax13b  2040  19.3t  2199  sb3bOLD  2482  cgsexg  3450  cgsex2g  3451  cgsex4g  3452  cgsex4gOLD  3453  elab3gf  3593  elab3g  3594  abidnf  3616  reuan  3808  sscon34b  4209  elsn2g  4579  eqoreldif  4600  difsn  4711  elpreqprb  4778  dfnfc2  4843  intmin4  4888  dfiin2g  4941  elpw2g  5237  ssrel  5654  ssrel2  5656  ssrelrel  5666  dmopab2rex  5786  releldmb  5815  relelrnb  5816  cnveqb  6059  dmsnopg  6076  relcnvtrg  6130  elsnxp  6154  ord0eln0  6267  f1ocnvb  6674  ffvresb  6941  isof1oopb  7134  soisores  7136  riotaclb  7212  fnoprabg  7333  difex2  7545  dfwe2  7559  ordpwsuc  7594  ordunisuc2  7623  limsssuc  7629  dfom2  7646  relcnvexb  7704  dfsmo2  8084  omord  8296  nneob  8381  fsetcdmex  8544  pw2f1olem  8749  sucdom  8875  fundmfibi  8955  f1dmvrnfibi  8960  fieq0  9037  hartogslem1  9158  rankr1ag  9418  rankeq0b  9476  fidomtri  9609  fidomtri2  9610  isfin2-2  9933  enfin2i  9935  isfin3-2  9981  isf34lem6  9994  isfin1-2  9999  isfin1-3  10000  isfin7-2  10010  axgroth6  10442  ltsonq  10583  ltexnq  10589  znegclb  12214  rpneg  12618  nltpnft  12754  ngtmnft  12756  xrrebnd  12758  qextlt  12793  qextle  12794  iccneg  13060  fzsn  13154  fz1sbc  13188  fzofzp1b  13340  ceilidz  13425  fleqceilz  13427  hashclb  13925  hashnncl  13933  hashfun  14004  reim0b  14682  rexanre  14910  rexuzre  14916  lo1resb  15125  o1resb  15127  dvdsext  15882  zob  15920  ncoprmgcdne1b  16207  pceq0  16424  pc11  16433  pcz  16434  ramtcl  16563  cshwsiun  16653  oduposb  17835  pospo  17851  cnvpsb  18085  tsrlemax  18092  issubg2  18558  issubg4  18562  ghmmhmb  18633  pmtrmvd  18848  mndodcong  18934  issubrg2  19820  lpigen  20294  cyggic  20537  ip2eq  20615  maducoeval2  21537  eltg3  21859  bastop  21878  0top  21880  iscld3  21961  isclo2  21985  cnprest  22186  dfconn2  22316  comppfsc  22429  cmphaushmeo  22697  reghaus  22722  nrmhaus  22723  fbun  22737  fsubbas  22764  ufileu  22816  uffix  22818  txflf  22903  fclsrest  22921  flimfnfcls  22925  ptcmplem2  22950  tgpt1  23015  tgpt0  23016  isngp2  23495  nrgdomn  23569  nmhmcn  24017  iscmet3  24190  limcflf  24778  ply1nzb  25020  coe11  25147  dgreq0  25159  eldmgm  25904  sqf11  26021  sqff1o  26064  zabsle1  26177  lgsabs1  26217  lgsquadlem2  26262  issubgr2  27360  uhgrissubgr  27363  usgrfilem  27415  uvtxnbgrb  27489  nbusgrvtxm1uvtx  27493  cusgrfilem3  27545  vdiscusgr  27619  wwlksn0s  27945  clwwlknon1loop  28181  clwwlknun  28195  nmobndi  28856  hmopadj2  30022  mdslle1i  30398  mdslle2i  30399  relfi  30660  ssrelf  30674  prodindf  31703  bnj1173  32695  revwlkb  32800  resconn  32921  cvmsval  32941  fmlafvel  33060  dmopab3rexdif  33080  elmrsubrn  33195  onelssex  33376  funsseq  33461  madebday  33817  oldbday  33818  brcolinear  34098  outsideofeu  34170  lineunray  34186  nn0prpw  34249  bj-nfimexal  34544  bj-sngltag  34910  bj-elpwg  34962  bj-elsn0  35061  bj-opelid  35062  bj-opelidres  35067  bj-ideqg1  35070  bj-imdirval3  35090  bj-inftyexpiinj  35115  wl-ax11-lem2  35474  poimirlem26  35540  poimirlem27  35541  heicant  35549  cover2  35609  eqfnun  35617  isbndx  35677  isbnd2  35678  equivbnd2  35687  prdsbnd2  35690  elghomlem2OLD  35781  isdrngo3  35854  riotaclbgBAD  36705  lssatle  36766  opcon3b  36947  cdlemk33N  38660  cdlemk34  38661  ioin9i8  39895  wepwsolem  40570  rp-fakeimass  40804  iscard5  40826  cnvssb  40870  intimag  40941  ntrneiiso  41378  pm11.71  41688  pm14.122b  41714  pm14.123b  41717  iotavalb  41721  elixpconstg  42312  eliuniin  42322  eliuniin2  42342  climreeq  42829  f1cof1b  44241  rexrsb  44264  afv0nbfvbi  44315  dfafn5b  44325  elfz2z  44480  zeo2ALTV  44796  fpprwpprb  44865  nnlog2ge0lt1  45585