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  361  bimsc1  841  biorf  934  pm4.72  947  19.38a  1843  19.38b  1844  ax13b  2036  19.3t  2195  sb3bOLD  2484  cgsexg  3475  cgsex2g  3476  cgsex4g  3477  cgsex4gOLD  3478  elab3gf  3616  elab3g  3617  abidnf  3639  reuan  3830  sscon34b  4229  elsn2g  4600  eqoreldif  4621  difsn  4732  elpreqprb  4799  dfnfc2  4864  intmin4  4909  dfiin2g  4963  elpw2g  5269  ssrel  5694  ssrelOLD  5695  ssrel2  5697  ssrelrel  5708  dmopab2rex  5829  releldmb  5858  relelrnb  5859  cnveqb  6104  dmsnopg  6121  relcnvtrg  6174  elsnxp  6198  ord0eln0  6324  f1ocnvb  6738  ffvresb  7007  isof1oopb  7205  soisores  7207  riotaclb  7283  fnoprabg  7406  difex2  7619  dfwe2  7633  ordpwsuc  7671  ordunisuc2  7700  limsssuc  7706  dfom2  7723  relcnvexb  7782  dfsmo2  8187  ord1eln01  8335  ord2eln012  8336  omord  8408  nneob  8495  fsetcdmex  8660  pw2f1olem  8872  sucdom  9027  sucdomOLD  9028  fundmfibi  9107  f1dmvrnfibi  9112  fieq0  9189  hartogslem1  9310  rankr1ag  9569  rankeq0b  9627  fidomtri  9760  fidomtri2  9761  isfin2-2  10084  enfin2i  10086  isfin3-2  10132  isf34lem6  10145  isfin1-2  10150  isfin1-3  10151  isfin7-2  10161  axgroth6  10593  ltsonq  10734  ltexnq  10740  znegclb  12366  rpneg  12771  nltpnft  12907  ngtmnft  12909  xrrebnd  12911  qextlt  12946  qextle  12947  iccneg  13213  fzsn  13307  fz1sbc  13341  fzofzp1b  13494  ceilidz  13581  fleqceilz  13583  hashclb  14082  hashnncl  14090  hashfun  14161  reim0b  14839  rexanre  15067  rexuzre  15073  lo1resb  15282  o1resb  15284  dvdsext  16039  zob  16077  ncoprmgcdne1b  16364  pceq0  16581  pc11  16590  pcz  16591  ramtcl  16720  cshwsiun  16810  oduposb  18056  pospo  18072  cnvpsb  18306  tsrlemax  18313  issubg2  18779  issubg4  18783  ghmmhmb  18854  pmtrmvd  19073  mndodcong  19159  issubrg2  20053  lpigen  20536  cyggic  20789  ip2eq  20867  maducoeval2  21798  eltg3  22121  bastop  22140  0top  22142  iscld3  22224  isclo2  22248  cnprest  22449  dfconn2  22579  comppfsc  22692  cmphaushmeo  22960  reghaus  22985  nrmhaus  22986  fbun  23000  fsubbas  23027  ufileu  23079  uffix  23081  txflf  23166  fclsrest  23184  flimfnfcls  23188  ptcmplem2  23213  tgpt1  23278  tgpt0  23279  isngp2  23762  nrgdomn  23844  nmhmcn  24292  iscmet3  24466  limcflf  25054  ply1nzb  25296  coe11  25423  dgreq0  25435  eldmgm  26180  sqf11  26297  sqff1o  26340  zabsle1  26453  lgsabs1  26493  lgsquadlem2  26538  issubgr2  27648  uhgrissubgr  27651  usgrfilem  27703  uvtxnbgrb  27777  nbusgrvtxm1uvtx  27781  cusgrfilem3  27833  vdiscusgr  27907  wwlksn0s  28235  clwwlknon1loop  28471  clwwlknun  28485  nmobndi  29146  hmopadj2  30312  mdslle1i  30688  mdslle2i  30689  relfi  30950  ssrelf  30964  prodindf  32000  bnj1173  32991  revwlkb  33096  resconn  33217  cvmsval  33237  fmlafvel  33356  dmopab3rexdif  33376  elmrsubrn  33491  onelssex  33670  funsseq  33751  madebday  34089  oldbday  34090  brcolinear  34370  outsideofeu  34442  lineunray  34458  nn0prpw  34521  bj-nfimexal  34816  bj-sngltag  35182  bj-elpwg  35234  bj-elsn0  35335  bj-opelid  35336  bj-opelidres  35341  bj-ideqg1  35344  bj-imdirval3  35364  bj-inftyexpiinj  35389  wl-ax11-lem2  35746  poimirlem26  35812  poimirlem27  35813  heicant  35821  cover2  35881  eqfnun  35889  isbndx  35949  isbnd2  35950  equivbnd2  35959  prdsbnd2  35962  elghomlem2OLD  36053  isdrngo3  36126  riotaclbgBAD  36975  lssatle  37036  opcon3b  37217  cdlemk33N  38930  cdlemk34  38931  ioin9i8  40180  wepwsolem  40874  rp-fakeimass  41126  iscard5  41150  cnvssb  41201  intimag  41271  ntrneiiso  41708  pm11.71  42022  pm14.122b  42048  pm14.123b  42051  iotavalb  42055  elixpconstg  42646  eliuniin  42656  eliuniin2  42676  climreeq  43161  f1cof1b  44580  rexrsb  44603  afv0nbfvbi  44654  dfafn5b  44664  elfz2z  44818  zeo2ALTV  45134  fpprwpprb  45203  nnlog2ge0lt1  45923