Theorem impbid2 229

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biimt  363  bimsc1  858  biorf  950  pm4.72  964  19.38a  1873  19.38b  1874  ax13b  2065  19.3t  2237  cgsexg  3494  cgsex2g  3495  cgsex4g  3496  elab3gf  3638  elab3g  3639  abidnf  3660  reuan  3844  sscon34b  4250  r19.3rzv  4459  elsn2g  4625  eqoreldif  4646  difsn  4761  elpreqprb  4828  dfnfc2  4889  intmin4  4937  elpw2g  5298  ssrel  5763  ssrel2  5765  ssrelrel  5776  dmopab2rex  5901  releldmb  5930  relelrnb  5931  cnveqb  6190  dmsnopg  6209  relcnvtrgOLD  6264  elsnxp  6289  onelssex  6407  ord0eln0  6414  f1ocnvb  6832  eqfnun  7030  ffvresb  7120  isof1oopb  7327  soisores  7329  riotaclb  7412  fnoprabg  7537  difex2  7760  dfwe2  7774  ordpwsuc  7812  ordunisuc2  7841  limsssuc  7847  dfom2  7865  relcnvexb  7924  dfsmo2  8337  ord1eln01  8486  ord2eln012  8487  omord  8558  nneob  8647  fsetcdmex  8867  pw2f1olem  9082  pwssfi  9174  sucdom  9217  1sdom  9228  fundmfibi  9306  f1dmvrnfibi  9311  fieq0  9394  hartogslem1  9517  rankr1ag  9787  rankeq0b  9845  fidomtri  10001  fidomtri2  10002  pr2ne  10011  isfin2-2  10324  enfin2i  10326  isfin3-2  10372  isf34lem6  10385  isfin1-2  10390  isfin1-3  10391  isfin7-2  10401  axgroth6  10840  ltsonq  10981  ltexnq  10987  znegclb  12658  rpneg  13079  nltpnft  13219  ngtmnft  13221  xrrebnd  13223  qextlt  13258  qextle  13259  iccneg  13528  fzsn  13624  fz1sbc  13658  fzdif1  13663  fzofzp1b  13824  ceilidz  13916  fleqceilz  13918  hashclb  14425  hashnncl  14433  hashfun  14505  reim0b  15209  rexanre  15437  rexuzre  15443  lo1resb  15654  o1resb  15656  dvdsext  16414  zob  16452  ncoprmgcdne1b  16743  pceq0  16966  pc11  16975  pcz  16976  ramtcl  17105  cshwsiun  17194  oduposb  18418  pospo  18434  cnvpsb  18670  tsrlemax  18677  issubg2  19268  issubg4  19272  eqg0subg  19327  ghmmhmb  19357  pmtrmvd  19586  mndodcong  19672  issubrng2  20723  issubrg2  20757  isdrng5  20920  ring2idlqusb  21516  lpigen  21569  cyggic  21788  ip2eq  21869  maducoeval2  22865  eltg3  23190  bastop  23209  0top  23211  iscld3  23292  isclo2  23316  cnprest  23517  dfconn2  23647  comppfsc  23761  cmphaushmeo  24029  reghaus  24054  nrmhaus  24055  fbun  24069  fsubbas  24096  ufileu  24148  uffix  24150  txflf  24235  fclsrest  24253  flimfnfcls  24257  ptcmplem2  24282  tgpt1  24347  tgpt0  24348  isngp2  24826  nrgdomn  24900  nmhmcn  25351  iscmet3  25524  limcflf  26111  ply1nzb  26351  coe11  26482  dgreq0  26494  eldmgm  27261  sqf11  27378  sqff1o  27421  zabsle1  27535  lgsabs1  27575  lgsquadlem2  27620  madebday  28168  oldbday  28169  leslss  28177  oldfib  28645  z12negsclb  28749  bdayfin  28755  issubgr2  29735  uhgrissubgr  29738  usgrfilem  29790  uvtxnbgrb  29864  nbusgrvtxm1uvtx  29868  cusgrfilem3  29920  vdiscusgr  29994  wwlksn0s  30332  clwwlknon1loop  30571  clwwlknun  30585  nmobndi  31259  hmopadj2  32425  mdslle1i  32801  mdslle2i  32802  relfi  33078  ssrelf  33091  prodindf  33311  bnj1173  35514  r1filim  35615  revwlkb  35725  resconn  35828  cvmsval  35848  fmlafvel  35967  dmopab3rexdif  35987  elmrsubrn  36102  funsseq  36350  brcolinear  36642  outsideofeu  36714  lineunray  36730  nn0prpw  36945  ttcsnexbig  37143  bj-nfimexal  37342  bj-spvw  37368  bj-sngltag  37730  bj-elpwg  37799  bj-elsn0  37910  bj-opelid  37911  bj-opelidres  37916  bj-ideqg1  37919  bj-imdirval3  37939  bj-inftyexpiinj  37964  qdiff  38082  poimirlem26  38398  poimirlem27  38399  heicant  38407  cover2  38468  isbndx  38535  isbnd2  38536  equivbnd2  38545  prdsbnd2  38548  elghomlem2OLD  38639  isdrngo3  38712  riotaclbgBAD  39830  lssatle  39891  opcon3b  40072  cdlemk33N  41785  cdlemk34  41786  quadfac  43074  ioin9i8  43078  eu6w  43525  wepwsolem  43886  onsupmaxb  44083  rp-fakeimass  44355  iscard5  44379  cnvssb  44429  intimag  44499  ntrneiiso  44934  pm11.71  45224  pm14.122b  45250  pm14.123b  45253  iotavalb  45257  relwf  45793  elixpconstg  45924  eliuniin  45934  eliuniin2  45955  climreeq  46446  f1cof1b  47968  rexrsb  47991  afv0nbfvbi  48042  dfafn5b  48052  elfz2z  48206  zeo2ALTV  48590  fpprwpprb  48659  dfsclnbgr6  48777  nnlog2ge0lt1  49499  oppccatb  49945