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  844  biorf  936  pm4.72  951  19.38a  1840  19.38b  1841  ax13b  2032  19.3t  2202  cgsexg  3489  cgsex2g  3490  cgsex4g  3491  cgsex4gOLD  3492  elab3gf  3648  elab3g  3649  abidnf  3670  reuan  3856  sscon34b  4263  elsn2g  4624  eqoreldif  4645  difsn  4758  elpreqprb  4828  dfnfc2  4889  intmin4  4937  dfiin2g  4991  elpw2g  5283  ssrel  5737  ssrel2  5739  ssrelrel  5750  dmopab2rex  5871  releldmb  5899  relelrnb  5900  cnveqb  6157  dmsnopg  6174  relcnvtrg  6227  elsnxp  6252  onelssex  6369  ord0eln0  6376  f1ocnvb  6795  eqfnun  6991  ffvresb  7079  isof1oopb  7282  soisores  7284  riotaclb  7367  fnoprabg  7492  difex2  7716  dfwe2  7730  ordpwsuc  7770  ordunisuc2  7800  limsssuc  7806  dfom2  7824  relcnvexb  7882  dfsmo2  8293  ord1eln01  8437  ord2eln012  8438  omord  8509  nneob  8597  fsetcdmex  8813  pw2f1olem  9022  pwssfi  9118  sucdom  9160  1sdom  9171  fundmfibi  9263  f1dmvrnfibi  9268  fieq0  9348  hartogslem1  9471  rankr1ag  9731  rankeq0b  9789  fidomtri  9922  fidomtri2  9923  pr2ne  9933  isfin2-2  10248  enfin2i  10250  isfin3-2  10296  isf34lem6  10309  isfin1-2  10314  isfin1-3  10315  isfin7-2  10325  axgroth6  10757  ltsonq  10898  ltexnq  10904  znegclb  12546  rpneg  12961  nltpnft  13100  ngtmnft  13102  xrrebnd  13104  qextlt  13139  qextle  13140  iccneg  13409  fzsn  13503  fz1sbc  13537  fzdif1  13542  fzofzp1b  13702  ceilidz  13790  fleqceilz  13792  hashclb  14299  hashnncl  14307  hashfun  14378  reim0b  15061  rexanre  15289  rexuzre  15295  lo1resb  15506  o1resb  15508  dvdsext  16267  zob  16305  ncoprmgcdne1b  16596  pceq0  16818  pc11  16827  pcz  16828  ramtcl  16957  cshwsiun  17046  oduposb  18268  pospo  18284  cnvpsb  18520  tsrlemax  18527  issubg2  19055  issubg4  19059  eqg0subg  19110  ghmmhmb  19141  pmtrmvd  19370  mndodcong  19456  issubrng2  20478  issubrg2  20512  ring2idlqusb  21252  lpigen  21277  cyggic  21514  ip2eq  21595  maducoeval2  22560  eltg3  22882  bastop  22901  0top  22903  iscld3  22984  isclo2  23008  cnprest  23209  dfconn2  23339  comppfsc  23452  cmphaushmeo  23720  reghaus  23745  nrmhaus  23746  fbun  23760  fsubbas  23787  ufileu  23839  uffix  23841  txflf  23926  fclsrest  23944  flimfnfcls  23948  ptcmplem2  23973  tgpt1  24038  tgpt0  24039  isngp2  24518  nrgdomn  24592  nmhmcn  25053  iscmet3  25226  limcflf  25815  ply1nzb  26061  coe11  26191  dgreq0  26204  eldmgm  26965  sqf11  27082  sqff1o  27125  zabsle1  27240  lgsabs1  27280  lgsquadlem2  27325  madebday  27849  oldbday  27850  slelss  27858  zs12negsclb  28393  issubgr2  29252  uhgrissubgr  29255  usgrfilem  29307  uvtxnbgrb  29381  nbusgrvtxm1uvtx  29385  cusgrfilem3  29438  vdiscusgr  29512  wwlksn0s  29841  clwwlknon1loop  30077  clwwlknun  30091  nmobndi  30754  hmopadj2  31920  mdslle1i  32296  mdslle2i  32297  relfi  32581  ssrelf  32593  prodindf  32836  bnj1173  34985  revwlkb  35106  resconn  35226  cvmsval  35246  fmlafvel  35365  dmopab3rexdif  35385  elmrsubrn  35500  funsseq  35748  brcolinear  36040  outsideofeu  36112  lineunray  36128  nn0prpw  36304  bj-nfimexal  36607  bj-sngltag  36964  bj-elpwg  37033  bj-elsn0  37136  bj-opelid  37137  bj-opelidres  37142  bj-ideqg1  37145  bj-imdirval3  37165  bj-inftyexpiinj  37190  wl-ax11-lem2  37567  poimirlem26  37633  poimirlem27  37634  heicant  37642  cover2  37702  isbndx  37769  isbnd2  37770  equivbnd2  37779  prdsbnd2  37782  elghomlem2OLD  37873  isdrngo3  37946  riotaclbgBAD  38940  lssatle  39001  opcon3b  39182  cdlemk33N  40896  cdlemk34  40897  ioin9i8  42188  eu6w  42657  wepwsolem  43024  onsupmaxb  43221  rp-fakeimass  43494  iscard5  43518  cnvssb  43568  intimag  43638  ntrneiiso  44073  pm11.71  44379  pm14.122b  44405  pm14.123b  44408  iotavalb  44412  relwf  44950  elixpconstg  45076  eliuniin  45086  eliuniin2  45107  climreeq  45604  f1cof1b  47071  rexrsb  47094  afv0nbfvbi  47145  dfafn5b  47155  elfz2z  47309  zeo2ALTV  47665  fpprwpprb  47734  dfsclnbgr6  47851  nnlog2ge0lt1  48548  oppccatb  48998