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 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biimt  363  bimsc1  858  biorf  950  pm4.72  964  19.38a  1873  19.38b  1874  ax13b  2065  19.3t  2238  cgsexg  3495  cgsex2g  3496  cgsex4g  3497  elab3gf  3638  elab3g  3639  abidnf  3660  reuan  3844  sscon34b  4250  r19.3rzv  4459  elsn2g  4625  eqoreldif  4646  difsn  4761  elpreqprb  4828  dfnfc2  4889  intmin4  4937  elpw2g  5295  ssrel  5759  ssrel2  5761  ssrelrel  5772  dmopab2rex  5899  releldmb  5928  relelrnb  5929  cnvssb  6189  cnveqb  6190  dmsnopg  6214  relcnvtrgOLD  6269  elsnxp  6294  onelssex  6412  ord0eln0  6419  f1ocnvb  6838  eqfnun  7036  ffvresb  7126  isof1oopb  7333  soisores  7335  riotaclb  7418  fnoprabg  7543  difex2  7774  dfwe2  7788  ordpwsuc  7826  ordunisuc2  7855  limsssuc  7861  dfom2  7879  relcnvexb  7938  dfsmo2  8355  ord1eln01  8504  ord2eln012  8505  omord  8576  nneob  8665  fsetcdmex  8885  pw2f1olem  9100  pwssfi  9192  sucdom  9235  1sdom  9246  fundmfibi  9325  f1dmvrnfibi  9330  fieq0  9413  hartogslem1  9536  rankr1ag  9810  rankeq0b  9876  fidomtri  10074  fidomtri2  10075  pr2ne  10084  isfin2-2  10397  enfin2i  10399  isfin3-2  10445  isf34lem6  10458  isfin1-2  10463  isfin1-3  10464  isfin7-2  10474  axgroth6  10913  ltsonq  11054  ltexnq  11060  znegclb  12733  rpneg  13154  nltpnft  13294  ngtmnft  13296  xrrebnd  13298  qextlt  13333  qextle  13334  iccneg  13603  fzsn  13700  fz1sbc  13734  fzdif1  13739  fzofzp1b  13900  ceilidz  13992  fleqceilz  13994  hashclb  14502  hashnncl  14510  hashfun  14582  reim0b  15286  rexanre  15514  rexuzre  15520  lo1resb  15731  o1resb  15733  dvdsext  16491  zob  16529  ncoprmgcdne1b  16825  pceq0  17049  pc11  17058  pcz  17059  ramtcl  17188  cshwsiun  17277  oduposb  18501  pospo  18517  cnvpsb  18753  tsrlemax  18760  issubg2  19352  issubg4  19356  eqg0subg  19411  ghmmhmb  19441  pmtrmvd  19670  mndodcong  19756  issubrng2  20810  issubrg2  20844  isdrng5  21008  ring2idlqusb  21606  lpigen  21659  cyggic  21878  ip2eq  21959  maducoeval2  22955  eltg3  23280  bastop  23299  0top  23301  iscld3  23382  isclo2  23406  cnprest  23607  dfconn2  23737  comppfsc  23851  cmphaushmeo  24119  reghaus  24144  nrmhaus  24145  fbun  24159  fsubbas  24186  ufileu  24238  uffix  24240  txflf  24325  fclsrest  24343  flimfnfcls  24347  ptcmplem2  24372  tgpt1  24437  tgpt0  24438  isngp2  24916  nrgdomn  24990  nmhmcn  25441  iscmet3  25614  limcflf  26201  ply1nzb  26441  coe11  26572  dgreq0  26584  eldmgm  27349  sqf11  27466  sqff1o  27509  zabsle1  27623  lgsabs1  27663  lgsquadlem2  27708  madebday  28286  oldbday  28287  leslss  28295  oldfib  28763  z12negsclb  28867  bdayfin  28873  issubgr2  29853  uhgrissubgr  29856  usgrfilem  29908  uvtxnbgrb  29982  nbusgrvtxm1uvtx  29986  cusgrfilem3  30038  vdiscusgr  30112  wwlksn0s  30450  clwwlknon1loop  30689  clwwlknun  30703  nmobndi  31377  hmopadj2  32543  mdslle1i  32919  mdslle2i  32920  relfi  33196  ssrelf  33209  prodindf  33429  bnj1173  35632  r1filim  35729  revwlkb  35908  resconn  36011  cvmsval  36031  fmlafvel  36150  dmopab3rexdif  36170  elmrsubrn  36285  funsseq  36533  brcolinear  36824  outsideofeu  36896  lineunray  36912  nn0prpw  37111  ttcsnexbig  37309  bj-nfimexal  37508  bj-spvw  37534  bj-sngltag  37896  bj-elpwg  37967  bj-elsn0  38076  bj-opelid  38077  bj-opelidres  38082  bj-ideqg1  38085  bj-imdirval3  38105  bj-inftyexpiinj  38130  qdiff  38248  poimirlem26  38564  poimirlem27  38565  heicant  38573  cover2  38649  isbndx  38716  isbnd2  38717  equivbnd2  38726  prdsbnd2  38729  elghomlem2OLD  38820  isdrngo3  38893  riotaclbgBAD  40011  lssatle  40072  opcon3b  40253  cdlemk33N  41966  cdlemk34  41967  quadfac  43255  ioin9i8  43259  eu6w  43687  wepwsolem  44048  onsupmaxb  44240  rp-fakeimass  44512  iscard5  44536  intimag  44655  ntrneiiso  45090  pm11.71  45380  pm14.122b  45406  pm14.123b  45409  iotavalb  45413  relwf  45956  hfrel  46019  elixpconstg  46103  eliuniin  46113  eliuniin2  46134  climreeq  46624  f1cof1b  48146  rexrsb  48169  afv0nbfvbi  48220  dfafn5b  48230  elfz2z  48384  zeo2ALTV  48768  fpprwpprb  48837  dfsclnbgr6  48955  nnlog2ge0lt1  49677  oppccatb  50123