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  2067  19.3t  2241  cgsexg  3498  cgsex2g  3499  cgsex4g  3500  elab3gf  3641  elab3g  3642  abidnf  3663  reuan  3848  sscon34b  4252  r19.3rzv  4462  elsn2g  4626  eqoreldif  4647  difsn  4763  elpreqprb  4828  dfnfc2  4894  intmin4  4942  elpw2g  5302  ssrel  5767  ssrelOLD  5768  ssrel2  5770  ssrelrel  5781  dmopab2rex  5911  releldmb  5940  relelrnb  5941  cnvssb  6207  dmsnopg  6233  relcnvtrgOLD  6293  elsnxp  6320  onelssex  6438  ord0eln0  6445  f1ocnvb  6868  eqfnun  7067  ffvresb  7158  isof1oopb  7364  soisores  7366  riotaclb  7449  fnoprabg  7574  difex2  7806  dfwe2  7820  ordpwsuc  7860  ordunisuc2  7889  limsssuc  7895  dfom2  7913  relcnvexb  7972  dfsmo2  8393  ord1eln01  8542  ord2eln012  8543  omord  8614  nneob  8703  fsetcdmex  8923  pw2f1olem  9138  pwssfi  9230  sucdom  9273  1sdom  9284  fundmfibi  9363  f1dmvrnfibi  9368  fieq0  9450  hartogslem1  9573  rankr1ag  9847  rankeq0b  9913  fidomtri  10113  fidomtri2  10114  pr2ne  10123  isfin2-2  10436  enfin2i  10438  isfin3-2  10484  isf34lem6  10497  isfin1-2  10502  isfin1-3  10503  isfin7-2  10513  axgroth6  10952  ltsonq  11093  ltexnq  11099  znegclb  12773  rpneg  13194  nltpnft  13334  ngtmnft  13336  xrrebnd  13338  qextlt  13373  qextle  13374  iccneg  13643  fzsn  13740  fz1sbc  13774  fzdif1  13779  fzofzp1b  13940  ceilidz  14032  fleqceilz  14034  hashclb  14543  hashnncl  14551  hashfun  14623  reim0b  15329  rexanre  15558  rexuzre  15564  lo1resb  15775  o1resb  15777  dvdsext  16535  zob  16573  ncoprmgcdne1b  16869  pceq0  17093  pc11  17102  pcz  17103  ramtcl  17232  cshwsiun  17321  oduposb  18551  pospo  18567  cnvpsb  18803  tsrlemax  18810  issubg2  19402  issubg4  19406  eqg0subg  19461  ghmmhmb  19491  pmtrmvd  19721  mndodcong  19807  issubrng2  20861  issubrg2  20895  isdrng5  21059  ring2idlqusb  21657  lpigen  21710  cyggic  21933  ip2eq  22014  maducoeval2  23010  eltg3  23335  bastop  23354  0top  23356  iscld3  23437  isclo2  23461  cnprest  23662  dfconn2  23792  comppfsc  23906  cmphaushmeo  24174  reghaus  24199  nrmhaus  24200  fbun  24214  fsubbas  24241  ufileu  24293  uffix  24295  txflf  24380  fclsrest  24398  flimfnfcls  24402  ptcmplem2  24427  tgpt1  24492  tgpt0  24493  isngp2  24971  nrgdomn  25045  nmhmcn  25496  iscmet3  25669  limcflf  26256  ply1nzb  26496  coe11  26627  dgreq0  26639  eldmgm  27406  sqf11  27523  sqff1o  27566  zabsle1  27680  lgsabs1  27720  lgsquadlem2  27765  madebday  28343  oldbday  28344  leslss  28352  oldfib  28820  z12negsclb  28924  bdayfin  28930  issubgr2  29910  uhgrissubgr  29913  usgrfilem  29965  uvtxnbgrb  30039  nbusgrvtxm1uvtx  30043  cusgrfilem3  30095  vdiscusgr  30169  wwlksn0s  30507  clwwlknon1loop  30746  clwwlknun  30760  nmobndi  31434  hmopadj2  32600  mdslle1i  32976  mdslle2i  32977  relfi  33294  ssrelf  33307  prodindf  33525  bnj1173  35743  r1filim  35854  revwlkb  36106  resconn  36219  cvmsval  36239  fmlafvel  36358  dmopab3rexdif  36378  elmrsubrn  36493  funsseq  36748  brcolinear  37039  outsideofeu  37111  lineunray  37127  nn0prpw  37326  ttcsnexbig  37524  bj-nfimexal  37723  bj-spvw  37749  bj-sngltag  38111  bj-ssrel  38175  cossididresb  38227  bj-elpwg  38237  bj-elsn0  38344  bj-opelid  38345  bj-opelidres  38350  bj-ideqg1  38353  bj-imdirval3  38373  bj-inftyexpiinj  38398  qdiff  38516  poimirlem26  38832  poimirlem27  38833  heicant  38841  cover2  38917  isbndx  38982  isbnd2  38983  equivbnd2  38992  prdsbnd2  38995  elghomlem2OLD  39086  isdrngo3  39159  riotaclbgBAD  40277  lssatle  40338  opcon3b  40519  cdlemk33N  42232  cdlemk34  42233  quadfac  43521  ioin9i8  43525  eu6w  43953  wepwsolem  44315  onsupmaxb  44502  rp-fakeimass  44774  iscard5  44798  intimag  44917  ntrneiiso  45352  pm11.71  45642  pm14.122b  45667  pm14.123b  45670  iotavalb  45674  relwf  46221  hfrel  46284  elixpconstg  46377  eliuniin  46387  eliuniin2  46408  climreeq  46898  f1cof1b  48420  rexrsb  48444  afv0nbfvbi  48494  dfafn5b  48504  elfz2z  48658  zeo2ALTV  49042  fpprwpprb  49111  dfsclnbgr6  49229  nnlog2ge0lt1  50009  oppccatb  50461