Theorem impbid2 228

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  biimt  363  bimsc1  840  biorf  933  pm4.72  946  19.38a  1840  19.38b  1841  ax13b  2039  19.3t  2201  sb3bOLD  2508  cgsexg  3537  cgsex2g  3538  cgsex4g  3539  elab3gf  3672  abidnf  3694  reuan  3880  elsn2g  4603  eqoreldif  4622  difsn  4731  elpreqprb  4798  dfnfc2  4860  intmin4  4905  dfiin2g  4957  elpw2g  5247  ssrel  5657  ssrel2  5659  ssrelrel  5669  dmopab2rex  5786  releldmb  5816  relelrnb  5817  cnveqb  6053  dmsnopg  6070  relcnvtrg  6119  elsnxp  6142  ord0eln0  6245  f1ocnvb  6628  ffvresb  6888  isof1oopb  7078  soisores  7080  riotaclb  7155  fnoprabg  7275  difex2  7482  dfwe2  7496  ordpwsuc  7530  ordunisuc2  7559  limsssuc  7565  dfom2  7582  relcnvexb  7631  dfsmo2  7984  omord  8194  nneob  8279  pw2f1olem  8621  sucdom  8715  fundmfibi  8803  f1dmvrnfibi  8808  fieq0  8885  hartogslem1  9006  rankr1ag  9231  rankeq0b  9289  fidomtri  9422  fidomtri2  9423  isfin2-2  9741  enfin2i  9743  isfin3-2  9789  isf34lem6  9802  isfin1-2  9807  isfin1-3  9808  isfin7-2  9818  axgroth6  10250  ltsonq  10391  ltexnq  10397  znegclb  12020  rpneg  12422  nltpnft  12558  ngtmnft  12560  xrrebnd  12562  qextlt  12597  qextle  12598  iccneg  12859  fzsn  12950  fz1sbc  12984  fzofzp1b  13136  ceilidz  13221  fleqceilz  13223  hashclb  13720  hashnncl  13728  hashfun  13799  reim0b  14478  rexanre  14706  rexuzre  14712  lo1resb  14921  o1resb  14923  dvdsext  15671  zob  15708  ncoprmgcdne1b  15994  pceq0  16207  pc11  16216  pcz  16217  ramtcl  16346  cshwsiun  16433  pospo  17583  oduposb  17746  cnvpsb  17823  tsrlemax  17830  issubg2  18294  issubg4  18298  ghmmhmb  18369  pmtrmvd  18584  mndodcong  18670  issubrg2  19555  lpigen  20029  cyggic  20719  ip2eq  20797  maducoeval2  21249  eltg3  21570  bastop  21589  0top  21591  iscld3  21672  isclo2  21696  cnprest  21897  dfconn2  22027  comppfsc  22140  cmphaushmeo  22408  reghaus  22433  nrmhaus  22434  fbun  22448  fsubbas  22475  ufileu  22527  uffix  22529  txflf  22614  fclsrest  22632  flimfnfcls  22636  ptcmplem2  22661  tgpt1  22726  tgpt0  22727  isngp2  23206  nrgdomn  23280  nmhmcn  23724  iscmet3  23896  limcflf  24479  ply1nzb  24716  coe11  24843  dgreq0  24855  eldmgm  25599  sqf11  25716  sqff1o  25759  zabsle1  25872  lgsabs1  25912  lgsquadlem2  25957  issubgr2  27054  uhgrissubgr  27057  usgrfilem  27109  uvtxnbgrb  27183  nbusgrvtxm1uvtx  27187  cusgrfilem3  27239  vdiscusgr  27313  wwlksn0s  27639  clwwlknon1loop  27877  clwwlknun  27891  nmobndi  28552  hmopadj2  29718  mdslle1i  30094  mdslle2i  30095  relfi  30352  ssrelf  30366  prodindf  31282  bnj1173  32274  revwlkb  32372  resconn  32493  cvmsval  32513  fmlafvel  32632  dmopab3rexdif  32652  elmrsubrn  32767  funsseq  33011  brcolinear  33520  outsideofeu  33592  lineunray  33608  nn0prpw  33671  bj-nfimexal  33959  bj-sngltag  34298  bj-elpwg  34348  bj-elsn0  34450  bj-opelid  34451  bj-opelidres  34456  bj-ideqg1  34459  bj-imdirval3  34477  bj-imdirid  34478  bj-inftyexpiinj  34494  wl-ax11-lem2  34833  poimirlem26  34933  poimirlem27  34934  heicant  34942  cover2  35004  eqfnun  35012  isbndx  35075  isbnd2  35076  equivbnd2  35085  prdsbnd2  35088  elghomlem2OLD  35179  isdrngo3  35252  riotaclbgBAD  36105  lssatle  36166  opcon3b  36347  cdlemk33N  38060  cdlemk34  38061  ioin9i8  39148  wepwsolem  39691  rp-fakeimass  39927  iscard5  39950  cnvssb  39995  intimag  40050  sscon34b  40418  ntrneiiso  40490  pm11.71  40778  pm14.122b  40804  pm14.123b  40807  iotavalb  40811  elixpconstg  41404  eliuniin  41414  eliuniin2  41435  climreeq  41943  rexrsb  43347  afv0nbfvbi  43399  dfafn5b  43409  elfz2z  43564  zeo2ALTV  43885  fpprwpprb  43954  nnlog2ge0lt1  44675