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  362  bimsc1  839  biorf  931  pm4.72  944  19.38a  1822  19.38b  1823  ax13b  2017  19.3t  2165  sb3b  2461  cgsexg  3479  cgsex2g  3480  cgsex4g  3481  elab3gf  3609  abidnf  3631  reuan  3810  elsn2g  4510  eqoreldif  4531  difsn  4640  elpreqprb  4707  dfnfc2  4765  intmin4  4813  dfiin2g  4862  elpw2g  5141  ssrel  5546  ssrel2  5548  ssrelrel  5558  dmopab2rex  5675  releldmb  5701  relelrnb  5702  cnveqb  5931  dmsnopg  5948  relcnvtrg  5997  elsnxp  6020  ord0eln0  6123  f1ocnvb  6499  ffvresb  6754  isof1oopb  6944  soisores  6946  riotaclb  7018  fnoprabg  7134  difex2  7342  dfwe2  7355  ordpwsuc  7389  ordunisuc2  7418  limsssuc  7424  dfom2  7441  relcnvexb  7490  dfsmo2  7839  omord  8047  nneob  8132  pw2f1olem  8471  sucdom  8564  fundmfibi  8652  f1dmvrnfibi  8657  fieq0  8734  hartogslem1  8855  rankr1ag  9080  rankeq0b  9138  fidomtri  9271  fidomtri2  9272  isfin2-2  9590  enfin2i  9592  isfin3-2  9638  isf34lem6  9651  isfin1-2  9656  isfin1-3  9657  isfin7-2  9667  axgroth6  10099  ltsonq  10240  ltexnq  10246  znegclb  11869  rpneg  12271  nltpnft  12407  ngtmnft  12409  xrrebnd  12411  qextlt  12446  qextle  12447  iccneg  12708  fzsn  12799  fz1sbc  12833  fzofzp1b  12985  ceilidz  13070  fleqceilz  13072  hashclb  13569  hashnncl  13577  hashfun  13646  reim0b  14312  rexanre  14540  rexuzre  14546  lo1resb  14755  o1resb  14757  dvdsext  15504  zob  15541  ncoprmgcdne1b  15823  pceq0  16036  pc11  16045  pcz  16046  ramtcl  16175  cshwsiun  16262  pospo  17412  oduposb  17575  cnvpsb  17652  tsrlemax  17659  issubg2  18048  issubg4  18052  ghmmhmb  18110  pmtrmvd  18315  mndodcong  18401  issubrg2  19245  lpigen  19718  cyggic  20401  ip2eq  20479  maducoeval2  20933  eltg3  21254  bastop  21273  0top  21275  iscld3  21356  isclo2  21380  cnprest  21581  dfconn2  21711  comppfsc  21824  cmphaushmeo  22092  reghaus  22117  nrmhaus  22118  fbun  22132  fsubbas  22159  ufileu  22211  uffix  22213  txflf  22298  fclsrest  22316  flimfnfcls  22320  ptcmplem2  22345  tgpt1  22409  tgpt0  22410  isngp2  22889  nrgdomn  22963  nmhmcn  23407  iscmet3  23579  limcflf  24162  ply1nzb  24399  coe11  24526  dgreq0  24538  eldmgm  25281  sqf11  25398  sqff1o  25441  zabsle1  25554  lgsabs1  25594  lgsquadlem2  25639  issubgr2  26737  uhgrissubgr  26740  usgrfilem  26792  uvtxnbgrb  26866  nbusgrvtxm1uvtx  26870  cusgrfilem3  26922  vdiscusgr  26996  wwlksn0s  27321  clwwlknon1loop  27559  clwwlknun  27573  nmobndi  28235  hmopadj2  29401  mdslle1i  29777  mdslle2i  29778  relfi  30034  ssrelf  30048  prodindf  30891  bnj1173  31880  revwlkb  31975  resconn  32095  cvmsval  32115  fmlafvel  32234  dmopab3rexdif  32254  elmrsubrn  32369  funsseq  32613  brcolinear  33123  outsideofeu  33195  lineunray  33211  nn0prpw  33274  bj-sngltag  33913  bj-epelg  33972  bj-elid2  34041  bj-inftyexpiinj  34062  wl-ax11-lem2  34362  poimirlem26  34462  poimirlem27  34463  heicant  34471  cover2  34534  eqfnun  34542  isbndx  34605  isbnd2  34606  equivbnd2  34615  prdsbnd2  34618  elghomlem2OLD  34709  isdrngo3  34782  riotaclbgBAD  35634  lssatle  35695  opcon3b  35876  cdlemk33N  37589  cdlemk34  37590  ioin9i8  38642  wepwsolem  39140  rp-fakeimass  39376  iscard5  39399  cnvssb  39444  intimag  39499  sscon34b  39867  ntrneiiso  39939  pm11.71  40280  pm14.122b  40306  pm14.123b  40309  iotavalb  40313  elixpconstg  40907  eliuniin  40917  eliuniin2  40939  climreeq  41449  rexrsb  42828  afv0nbfvbi  42880  dfafn5b  42890  elfz2z  43045  zeo2ALTV  43332  fpprwpprb  43401  nnlog2ge0lt1  44121