Theorem impbid2 217

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 216	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
4	3	bicomd 214	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 197

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 198

This theorem is referenced by:  biimt  351  bimsc1  870  biort  959  biorf  960  pm4.72  972  19.38a  1934  19.38aOLD  1935  19.38b  1936  19.38bOLD  1937  ax13b  2132  19.3t  2232  sb3b  2446  cgsexg  3391  cgsex2g  3392  cgsex4g  3393  elab3gf  3513  abidnf  3534  elsn2g  4370  eqoreldif  4384  difsn  4485  prel12OLD  4536  elpreqprb  4556  dfnfc2  4616  intmin4  4664  dfiin2g  4711  elpw2g  4987  ssrel  5379  ssrel2  5381  ssrelrel  5391  releldmb  5531  relelrnb  5532  cnveqb  5775  dmsnopg  5792  relcnvtr  5843  elsnxp  5865  ord0eln0  5964  f1ocnvb  6337  ffvresb  6588  isof1oopb  6771  soisores  6773  riotaclb  6845  fnoprabg  6963  difex2  7171  dfwe2  7183  ordpwsuc  7217  ordunisuc2  7246  limsssuc  7252  dfom2  7269  relcnvexb  7316  dfsmo2  7652  omord  7857  nneob  7941  pw2f1olem  8275  sucdom  8368  fundmfibi  8456  f1dmvrnfibi  8461  fieq0  8538  hartogslem1  8658  rankr1ag  8884  rankeq0b  8942  fidomtri  9074  fidomtri2  9075  isfin2-2  9398  enfin2i  9400  isfin3-2  9446  isf34lem6  9459  isfin1-2  9464  isfin1-3  9465  isfin7-2  9475  axgroth6  9907  ltsonq  10048  ltexnq  10054  znegclb  11666  rpneg  12066  nltpnft  12202  ngtmnft  12204  xrrebnd  12206  qextlt  12241  qextle  12242  iccneg  12503  fzsn  12595  fz1sbc  12628  fzofzp1b  12779  ceilidz  12864  fleqceilz  12866  hashclb  13356  hashnncl  13364  hashfun  13430  reim0b  14158  rexanre  14385  rexuzre  14391  lo1resb  14594  o1resb  14596  dvdsext  15342  zob  15379  ncoprmgcdne1b  15658  pceq0  15868  pc11  15877  pcz  15878  ramtcl  16007  cshwsiun  16094  pospo  17253  oduposb  17416  cnvpsb  17493  tsrlemax  17500  issubg2  17887  issubg4  17891  ghmmhmb  17949  pmtrmvd  18153  mndodcong  18239  issubrg2  19083  lpigen  19544  cyggic  20207  ip2eq  20287  maducoeval2  20737  eltg3  21060  bastop  21079  0top  21081  iscld3  21162  isclo2  21186  cnprest  21387  dfconn2  21516  comppfsc  21629  cmphaushmeo  21897  reghaus  21922  nrmhaus  21923  fbun  21937  fsubbas  21964  ufileu  22016  uffix  22018  txflf  22103  fclsrest  22121  flimfnfcls  22125  ptcmplem2  22150  tgpt1  22214  tgpt0  22215  isngp2  22694  nrgdomn  22768  nmhmcn  23212  iscmet3  23384  limcflf  23950  ply1nzb  24187  coe11  24314  dgreq0  24326  eldmgm  25053  sqf11  25170  sqff1o  25213  zabsle1  25326  lgsabs1  25366  lgsquadlem2  25411  issubgr2  26457  uhgrissubgr  26460  usgrfilem  26512  uvtxnbgrb  26601  nbusgrvtxm1uvtx  26605  cusgrfilem3  26658  vdiscusgr  26732  wwlksn0s  27070  clwwlknon1loop  27389  clwwlknun  27404  nmobndi  28107  hmopadj2  29277  mdslle1i  29653  mdslle2i  29654  relfi  29884  ssrelf  29896  prodindf  30553  bnj1173  31539  resconn  31697  cvmsval  31717  elmrsubrn  31886  funsseq  32132  brcolinear  32631  outsideofeu  32703  lineunray  32719  nn0prpw  32782  bj-sngltag  33419  bj-elid2  33540  bj-inftyexpiinj  33551  wl-ax11-lem2  33809  poimirlem26  33880  poimirlem27  33881  heicant  33889  cover2  33952  eqfnun  33960  isbndx  34024  isbnd2  34025  equivbnd2  34034  prdsbnd2  34037  elghomlem2OLD  34128  isdrngo3  34201  riotaclbgBAD  34931  lssatle  34992  opcon3b  35173  cdlemk33N  36886  cdlemk34  36887  ioin9i8  37948  wepwsolem  38313  rp-fakeimass  38557  cnvssb  38591  intimag  38647  sscon34b  39015  ntrneiiso  39087  pm11.71  39295  pm14.122b  39321  pm14.123b  39324  iotavalb  39328  eliuniin  39954  eliuniin2  39977  climreeq  40507  rexrsb  41865  reuan  41875  afv0nbfvbi  41923  dfafn5b  41933  elfz2z  42083  zeo2ALTV  42282  nnlog2ge0lt1  43053