Theorem impbid2 226

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  biimt  360  bimsc1  843  biorf  935  pm4.72  950  19.38a  1838  19.38b  1839  ax13b  2031  19.3t  2202  cgsexg  3536  cgsex2g  3537  cgsex4g  3538  cgsex4gOLD  3539  elab3gf  3700  elab3g  3701  abidnf  3724  reuan  3918  sscon34b  4323  elsn2g  4686  eqoreldif  4708  difsn  4823  elpreqprb  4892  dfnfc2  4953  intmin4  5001  dfiin2g  5055  elpw2g  5351  ssrel  5806  ssrelOLD  5807  ssrel2  5809  ssrelrel  5820  dmopab2rex  5942  releldmb  5971  relelrnb  5972  cnveqb  6227  dmsnopg  6244  relcnvtrg  6297  elsnxp  6322  onelssex  6443  ord0eln0  6450  f1ocnvb  6875  eqfnun  7070  ffvresb  7159  isof1oopb  7361  soisores  7363  riotaclb  7446  fnoprabg  7573  difex2  7795  dfwe2  7809  ordpwsuc  7851  ordunisuc2  7881  limsssuc  7887  dfom2  7905  relcnvexb  7966  dfsmo2  8403  ord1eln01  8552  ord2eln012  8553  omord  8624  nneob  8712  fsetcdmex  8921  pw2f1olem  9142  sucdom  9298  sucdomOLD  9299  1sdom  9311  fundmfibi  9404  f1dmvrnfibi  9409  fieq0  9490  hartogslem1  9611  rankr1ag  9871  rankeq0b  9929  fidomtri  10062  fidomtri2  10063  pr2ne  10073  isfin2-2  10388  enfin2i  10390  isfin3-2  10436  isf34lem6  10449  isfin1-2  10454  isfin1-3  10455  isfin7-2  10465  axgroth6  10897  ltsonq  11038  ltexnq  11044  znegclb  12680  rpneg  13089  nltpnft  13226  ngtmnft  13228  xrrebnd  13230  qextlt  13265  qextle  13266  iccneg  13532  fzsn  13626  fz1sbc  13660  fzofzp1b  13815  ceilidz  13903  fleqceilz  13905  hashclb  14407  hashnncl  14415  hashfun  14486  reim0b  15168  rexanre  15395  rexuzre  15401  lo1resb  15610  o1resb  15612  dvdsext  16369  zob  16407  ncoprmgcdne1b  16697  pceq0  16918  pc11  16927  pcz  16928  ramtcl  17057  cshwsiun  17147  oduposb  18399  pospo  18415  cnvpsb  18649  tsrlemax  18656  issubg2  19181  issubg4  19185  eqg0subg  19236  ghmmhmb  19267  pmtrmvd  19498  mndodcong  19584  issubrng2  20584  issubrg2  20620  ring2idlqusb  21343  lpigen  21368  cyggic  21614  ip2eq  21694  maducoeval2  22667  eltg3  22990  bastop  23009  0top  23011  iscld3  23093  isclo2  23117  cnprest  23318  dfconn2  23448  comppfsc  23561  cmphaushmeo  23829  reghaus  23854  nrmhaus  23855  fbun  23869  fsubbas  23896  ufileu  23948  uffix  23950  txflf  24035  fclsrest  24053  flimfnfcls  24057  ptcmplem2  24082  tgpt1  24147  tgpt0  24148  isngp2  24631  nrgdomn  24713  nmhmcn  25172  iscmet3  25346  limcflf  25936  ply1nzb  26182  coe11  26312  dgreq0  26325  eldmgm  27083  sqf11  27200  sqff1o  27243  zabsle1  27358  lgsabs1  27398  lgsquadlem2  27443  madebday  27956  oldbday  27957  slelss  27964  issubgr2  29307  uhgrissubgr  29310  usgrfilem  29362  uvtxnbgrb  29436  nbusgrvtxm1uvtx  29440  cusgrfilem3  29493  vdiscusgr  29567  wwlksn0s  29894  clwwlknon1loop  30130  clwwlknun  30144  nmobndi  30807  hmopadj2  31973  mdslle1i  32349  mdslle2i  32350  relfi  32624  ssrelf  32637  prodindf  33987  bnj1173  34978  revwlkb  35093  resconn  35214  cvmsval  35234  fmlafvel  35353  dmopab3rexdif  35373  elmrsubrn  35488  funsseq  35731  brcolinear  36023  outsideofeu  36095  lineunray  36111  nn0prpw  36289  bj-nfimexal  36592  bj-sngltag  36949  bj-elpwg  37018  bj-elsn0  37121  bj-opelid  37122  bj-opelidres  37127  bj-ideqg1  37130  bj-imdirval3  37150  bj-inftyexpiinj  37175  wl-ax11-lem2  37540  poimirlem26  37606  poimirlem27  37607  heicant  37615  cover2  37675  isbndx  37742  isbnd2  37743  equivbnd2  37752  prdsbnd2  37755  elghomlem2OLD  37846  isdrngo3  37919  riotaclbgBAD  38910  lssatle  38971  opcon3b  39152  cdlemk33N  40866  cdlemk34  40867  ioin9i8  42201  eu6w  42631  wepwsolem  42999  onsupmaxb  43200  rp-fakeimass  43474  iscard5  43498  cnvssb  43548  intimag  43618  ntrneiiso  44053  pm11.71  44366  pm14.122b  44392  pm14.123b  44395  iotavalb  44399  elixpconstg  44991  eliuniin  45001  eliuniin2  45022  climreeq  45534  f1cof1b  46992  rexrsb  47015  afv0nbfvbi  47066  dfafn5b  47076  elfz2z  47230  zeo2ALTV  47545  fpprwpprb  47614  dfsclnbgr6  47730  nnlog2ge0lt1  48300