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  2239  cgsexg  3497  cgsex2g  3498  cgsex4g  3499  elab3gf  3641  elab3g  3642  abidnf  3663  reuan  3847  sscon34b  4253  r19.3rzv  4462  elsn2g  4628  eqoreldif  4649  difsn  4764  elpreqprb  4831  dfnfc2  4892  intmin4  4940  elpw2g  5302  ssrel  5767  ssrel2  5769  ssrelrel  5780  dmopab2rex  5905  releldmb  5934  relelrnb  5935  cnveqb  6194  dmsnopg  6213  relcnvtrgOLD  6268  elsnxp  6293  onelssex  6411  ord0eln0  6418  f1ocnvb  6835  eqfnun  7033  ffvresb  7123  isof1oopb  7330  soisores  7332  riotaclb  7415  fnoprabg  7540  difex2  7763  dfwe2  7777  ordpwsuc  7815  ordunisuc2  7844  limsssuc  7850  dfom2  7868  relcnvexb  7927  dfsmo2  8340  ord1eln01  8487  ord2eln012  8488  omord  8559  nneob  8648  fsetcdmex  8868  pw2f1olem  9083  pwssfi  9175  sucdom  9218  1sdom  9229  fundmfibi  9307  f1dmvrnfibi  9312  fieq0  9395  hartogslem1  9518  rankr1ag  9788  rankeq0b  9846  fidomtri  10002  fidomtri2  10003  pr2ne  10012  isfin2-2  10325  enfin2i  10327  isfin3-2  10373  isf34lem6  10386  isfin1-2  10391  isfin1-3  10392  isfin7-2  10402  axgroth6  10841  ltsonq  10982  ltexnq  10988  znegclb  12659  rpneg  13080  nltpnft  13220  ngtmnft  13222  xrrebnd  13224  qextlt  13259  qextle  13260  iccneg  13529  fzsn  13625  fz1sbc  13659  fzdif1  13664  fzofzp1b  13825  ceilidz  13917  fleqceilz  13919  hashclb  14426  hashnncl  14434  hashfun  14506  reim0b  15210  rexanre  15438  rexuzre  15444  lo1resb  15655  o1resb  15657  dvdsext  16417  zob  16455  ncoprmgcdne1b  16746  pceq0  16969  pc11  16978  pcz  16979  ramtcl  17108  cshwsiun  17197  oduposb  18421  pospo  18437  cnvpsb  18673  tsrlemax  18680  issubg2  19271  issubg4  19275  eqg0subg  19330  ghmmhmb  19360  pmtrmvd  19589  mndodcong  19675  issubrng2  20726  issubrg2  20760  isdrng5  20923  ring2idlqusb  21519  lpigen  21572  cyggic  21791  ip2eq  21872  maducoeval2  22868  eltg3  23193  bastop  23212  0top  23214  iscld3  23295  isclo2  23319  cnprest  23520  dfconn2  23650  comppfsc  23764  cmphaushmeo  24032  reghaus  24057  nrmhaus  24058  fbun  24072  fsubbas  24099  ufileu  24151  uffix  24153  txflf  24238  fclsrest  24256  flimfnfcls  24260  ptcmplem2  24285  tgpt1  24350  tgpt0  24351  isngp2  24829  nrgdomn  24903  nmhmcn  25354  iscmet3  25527  limcflf  26115  ply1nzb  26355  coe11  26486  dgreq0  26498  eldmgm  27266  sqf11  27383  sqff1o  27426  zabsle1  27540  lgsabs1  27580  lgsquadlem2  27625  madebday  28173  oldbday  28174  leslss  28182  oldfib  28650  z12negsclb  28754  bdayfin  28760  issubgr2  29740  uhgrissubgr  29743  usgrfilem  29795  uvtxnbgrb  29869  nbusgrvtxm1uvtx  29873  cusgrfilem3  29925  vdiscusgr  29999  wwlksn0s  30337  clwwlknon1loop  30576  clwwlknun  30590  nmobndi  31264  hmopadj2  32430  mdslle1i  32806  mdslle2i  32807  relfi  33083  ssrelf  33096  prodindf  33316  bnj1173  35519  r1filim  35620  revwlkb  35730  resconn  35833  cvmsval  35853  fmlafvel  35972  dmopab3rexdif  35992  elmrsubrn  36107  funsseq  36355  brcolinear  36647  outsideofeu  36719  lineunray  36735  nn0prpw  36950  ttcsnexbig  37148  bj-nfimexal  37347  bj-spvw  37373  bj-sngltag  37735  bj-elpwg  37804  bj-elsn0  37915  bj-opelid  37916  bj-opelidres  37921  bj-ideqg1  37924  bj-imdirval3  37944  bj-inftyexpiinj  37969  qdiff  38087  poimirlem26  38403  poimirlem27  38404  heicant  38412  cover2  38473  isbndx  38540  isbnd2  38541  equivbnd2  38550  prdsbnd2  38553  elghomlem2OLD  38644  isdrngo3  38717  riotaclbgBAD  39835  lssatle  39896  opcon3b  40077  cdlemk33N  41790  cdlemk34  41791  quadfac  43079  ioin9i8  43083  eu6w  43530  wepwsolem  43891  onsupmaxb  44088  rp-fakeimass  44360  iscard5  44384  cnvssb  44434  intimag  44504  ntrneiiso  44939  pm11.71  45229  pm14.122b  45255  pm14.123b  45258  iotavalb  45262  relwf  45798  elixpconstg  45929  eliuniin  45939  eliuniin2  45960  climreeq  46451  f1cof1b  47973  rexrsb  47996  afv0nbfvbi  48047  dfafn5b  48057  elfz2z  48211  zeo2ALTV  48595  fpprwpprb  48664  dfsclnbgr6  48782  nnlog2ge0lt1  49504  oppccatb  49950