Theorem impbid2 227

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  biimt  361  bimsc1  850  biorf  942  pm4.72  957  19.38a  1847  19.38b  1848  ax13b  2039  19.3t  2213  cgsexg  3475  cgsex2g  3476  cgsex4g  3477  elab3gf  3622  elab3g  3623  abidnf  3643  reuan  3828  sscon34b  4232  r19.3rzv  4431  elsn2g  4596  eqoreldif  4617  difsn  4731  elpreqprb  4799  dfnfc2  4860  intmin4  4907  elpw2g  5261  ssrel  5726  ssrel2  5728  ssrelrel  5739  dmopab2rex  5859  releldmb  5888  relelrnb  5889  cnveqb  6147  dmsnopg  6164  relcnvtrg  6218  elsnxp  6242  onelssex  6359  ord0eln0  6366  f1ocnvb  6780  eqfnun  6978  ffvresb  7067  isof1oopb  7269  soisores  7271  riotaclb  7354  fnoprabg  7479  difex2  7703  dfwe2  7717  ordpwsuc  7755  ordunisuc2  7784  limsssuc  7790  dfom2  7808  relcnvexb  7866  dfsmo2  8277  ord1eln01  8421  ord2eln012  8422  omord  8493  nneob  8582  fsetcdmex  8800  pw2f1olem  9009  pwssfi  9101  sucdom  9144  1sdom  9155  fundmfibi  9236  f1dmvrnfibi  9241  fieq0  9324  hartogslem1  9447  rankr1ag  9717  rankeq0b  9775  fidomtri  9908  fidomtri2  9909  pr2ne  9918  isfin2-2  10232  enfin2i  10234  isfin3-2  10280  isf34lem6  10293  isfin1-2  10298  isfin1-3  10299  isfin7-2  10309  axgroth6  10742  ltsonq  10883  ltexnq  10889  znegclb  12555  rpneg  12967  nltpnft  13107  ngtmnft  13109  xrrebnd  13111  qextlt  13146  qextle  13147  iccneg  13416  fzsn  13511  fz1sbc  13545  fzdif1  13550  fzofzp1b  13711  ceilidz  13802  fleqceilz  13804  hashclb  14311  hashnncl  14319  hashfun  14390  reim0b  15072  rexanre  15300  rexuzre  15306  lo1resb  15517  o1resb  15519  dvdsext  16281  zob  16319  ncoprmgcdne1b  16610  pceq0  16833  pc11  16842  pcz  16843  ramtcl  16972  cshwsiun  17061  oduposb  18284  pospo  18300  cnvpsb  18536  tsrlemax  18543  issubg2  19108  issubg4  19112  eqg0subg  19162  ghmmhmb  19193  pmtrmvd  19422  mndodcong  19508  issubrng2  20530  issubrg2  20564  ring2idlqusb  21303  lpigen  21328  cyggic  21547  ip2eq  21628  maducoeval2  22623  eltg3  22945  bastop  22964  0top  22966  iscld3  23047  isclo2  23071  cnprest  23272  dfconn2  23402  comppfsc  23515  cmphaushmeo  23783  reghaus  23808  nrmhaus  23809  fbun  23823  fsubbas  23850  ufileu  23902  uffix  23904  txflf  23989  fclsrest  24007  flimfnfcls  24011  ptcmplem2  24036  tgpt1  24101  tgpt0  24102  isngp2  24580  nrgdomn  24654  nmhmcn  25105  iscmet3  25278  limcflf  25866  ply1nzb  26106  coe11  26236  dgreq0  26248  eldmgm  27003  sqf11  27120  sqff1o  27163  zabsle1  27277  lgsabs1  27317  lgsquadlem2  27362  madebday  27910  oldbday  27911  leslss  27919  oldfib  28387  z12negsclb  28491  bdayfin  28497  issubgr2  29359  uhgrissubgr  29362  usgrfilem  29414  uvtxnbgrb  29488  nbusgrvtxm1uvtx  29492  cusgrfilem3  29544  vdiscusgr  29618  wwlksn0s  29947  clwwlknon1loop  30186  clwwlknun  30200  nmobndi  30864  hmopadj2  32030  mdslle1i  32406  mdslle2i  32407  relfi  32691  ssrelf  32707  prodindf  32941  bnj1173  35184  r1filim  35285  revwlkb  35354  resconn  35474  cvmsval  35494  fmlafvel  35613  dmopab3rexdif  35633  elmrsubrn  35748  funsseq  35996  brcolinear  36287  outsideofeu  36359  lineunray  36375  nn0prpw  36551  ttcsnexbig  36749  bj-nfimexal  36949  bj-spvw  36975  bj-sngltag  37336  bj-elpwg  37405  bj-elsn0  37515  bj-opelid  37516  bj-opelidres  37521  bj-ideqg1  37524  bj-imdirval3  37544  bj-inftyexpiinj  37569  qdiff  37687  poimirlem26  38013  poimirlem27  38014  heicant  38022  cover2  38082  isbndx  38149  isbnd2  38150  equivbnd2  38159  prdsbnd2  38162  elghomlem2OLD  38253  isdrngo3  38326  riotaclbgBAD  39446  lssatle  39507  opcon3b  39688  cdlemk33N  41401  cdlemk34  41402  ioin9i8  42692  eu6w  43126  wepwsolem  43487  onsupmaxb  43684  rp-fakeimass  43956  iscard5  43980  cnvssb  44030  intimag  44100  ntrneiiso  44535  pm11.71  44841  pm14.122b  44867  pm14.123b  44870  iotavalb  44874  relwf  45411  elixpconstg  45536  eliuniin  45546  eliuniin2  45567  climreeq  46058  f1cof1b  47540  rexrsb  47563  afv0nbfvbi  47614  dfafn5b  47624  elfz2z  47778  zeo2ALTV  48162  fpprwpprb  48231  dfsclnbgr6  48349  nnlog2ge0lt1  49057  oppccatb  49506