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  1872  19.38b  1873  ax13b  2066  19.3t  2240  cgsexg  3497  cgsex2g  3498  cgsex4g  3499  elab3gf  3640  elab3g  3641  abidnf  3662  reuan  3847  sscon34b  4251  r19.3rzv  4461  elsn2g  4624  eqoreldif  4645  difsn  4760  elpreqprb  4825  dfnfc2  4891  intmin4  4939  elpw2g  5298  ssrel  5763  ssrel2  5765  ssrelrel  5776  dmopab2rex  5903  releldmb  5932  relelrnb  5933  cnvssb  6194  dmsnopg  6220  relcnvtrgOLD  6275  elsnxp  6300  onelssex  6418  ord0eln0  6425  f1ocnvb  6846  eqfnun  7044  ffvresb  7134  isof1oopb  7340  soisores  7342  riotaclb  7425  fnoprabg  7550  difex2  7781  dfwe2  7795  ordpwsuc  7833  ordunisuc2  7862  limsssuc  7868  dfom2  7886  relcnvexb  7945  dfsmo2  8366  ord1eln01  8515  ord2eln012  8516  omord  8587  nneob  8676  fsetcdmex  8896  pw2f1olem  9111  pwssfi  9203  sucdom  9246  1sdom  9257  fundmfibi  9336  f1dmvrnfibi  9341  fieq0  9423  hartogslem1  9546  rankr1ag  9820  rankeq0b  9886  fidomtri  10084  fidomtri2  10085  pr2ne  10094  isfin2-2  10407  enfin2i  10409  isfin3-2  10455  isf34lem6  10468  isfin1-2  10473  isfin1-3  10474  isfin7-2  10484  axgroth6  10923  ltsonq  11064  ltexnq  11070  znegclb  12743  rpneg  13164  nltpnft  13304  ngtmnft  13306  xrrebnd  13308  qextlt  13343  qextle  13344  iccneg  13613  fzsn  13710  fz1sbc  13744  fzdif1  13749  fzofzp1b  13910  ceilidz  14002  fleqceilz  14004  hashclb  14512  hashnncl  14520  hashfun  14592  reim0b  15298  rexanre  15526  rexuzre  15532  lo1resb  15743  o1resb  15745  dvdsext  16503  zob  16541  ncoprmgcdne1b  16837  pceq0  17061  pc11  17070  pcz  17071  ramtcl  17200  cshwsiun  17289  oduposb  18513  pospo  18529  cnvpsb  18765  tsrlemax  18772  issubg2  19364  issubg4  19368  eqg0subg  19423  ghmmhmb  19453  pmtrmvd  19682  mndodcong  19768  issubrng2  20822  issubrg2  20856  isdrng5  21020  ring2idlqusb  21618  lpigen  21671  cyggic  21890  ip2eq  21971  maducoeval2  22967  eltg3  23292  bastop  23311  0top  23313  iscld3  23394  isclo2  23418  cnprest  23619  dfconn2  23749  comppfsc  23863  cmphaushmeo  24131  reghaus  24156  nrmhaus  24157  fbun  24171  fsubbas  24198  ufileu  24250  uffix  24252  txflf  24337  fclsrest  24355  flimfnfcls  24359  ptcmplem2  24384  tgpt1  24449  tgpt0  24450  isngp2  24928  nrgdomn  25002  nmhmcn  25453  iscmet3  25626  limcflf  26213  ply1nzb  26453  coe11  26584  dgreq0  26596  eldmgm  27361  sqf11  27478  sqff1o  27521  zabsle1  27635  lgsabs1  27675  lgsquadlem2  27720  madebday  28298  oldbday  28299  leslss  28307  oldfib  28775  z12negsclb  28879  bdayfin  28885  issubgr2  29865  uhgrissubgr  29868  usgrfilem  29920  uvtxnbgrb  29994  nbusgrvtxm1uvtx  29998  cusgrfilem3  30050  vdiscusgr  30124  wwlksn0s  30462  clwwlknon1loop  30701  clwwlknun  30715  nmobndi  31389  hmopadj2  32555  mdslle1i  32931  mdslle2i  32932  relfi  33250  ssrelf  33263  prodindf  33482  bnj1173  35685  r1filim  35790  revwlkb  36019  resconn  36132  cvmsval  36152  fmlafvel  36271  dmopab3rexdif  36291  elmrsubrn  36406  funsseq  36660  brcolinear  36951  outsideofeu  37023  lineunray  37039  nn0prpw  37238  ttcsnexbig  37436  bj-nfimexal  37635  bj-spvw  37661  bj-sngltag  38023  bj-elpwg  38106  bj-elsn0  38216  bj-opelid  38217  bj-opelidres  38222  bj-ideqg1  38225  bj-imdirval3  38245  bj-inftyexpiinj  38270  qdiff  38388  poimirlem26  38704  poimirlem27  38705  heicant  38713  cover2  38789  isbndx  38856  isbnd2  38857  equivbnd2  38866  prdsbnd2  38869  elghomlem2OLD  38960  isdrngo3  39033  riotaclbgBAD  40151  lssatle  40212  opcon3b  40393  cdlemk33N  42106  cdlemk34  42107  quadfac  43395  ioin9i8  43399  eu6w  43827  wepwsolem  44189  onsupmaxb  44381  rp-fakeimass  44653  iscard5  44677  intimag  44796  ntrneiiso  45231  pm11.71  45521  pm14.122b  45546  pm14.123b  45549  iotavalb  45553  relwf  46096  hfrel  46159  elixpconstg  46243  eliuniin  46253  eliuniin2  46274  climreeq  46764  f1cof1b  48286  rexrsb  48310  afv0nbfvbi  48360  dfafn5b  48370  elfz2z  48524  zeo2ALTV  48908  fpprwpprb  48977  dfsclnbgr6  49095  nnlog2ge0lt1  49817  oppccatb  50269