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  2240  cgsexg  3501  cgsex2g  3502  cgsex4g  3503  elab3gf  3645  elab3g  3646  abidnf  3667  reuan  3851  sscon34b  4257  r19.3rzv  4466  elsn2g  4632  eqoreldif  4653  difsn  4768  elpreqprb  4835  dfnfc2  4896  intmin4  4944  elpw2g  5306  ssrel  5771  ssrel2  5773  ssrelrel  5784  dmopab2rex  5909  releldmb  5938  relelrnb  5939  cnveqb  6197  dmsnopg  6216  relcnvtrgOLD  6271  elsnxp  6296  onelssex  6414  ord0eln0  6421  f1ocnvb  6838  eqfnun  7036  ffvresb  7125  isof1oopb  7332  soisores  7334  riotaclb  7417  fnoprabg  7542  difex2  7765  dfwe2  7779  ordpwsuc  7817  ordunisuc2  7846  limsssuc  7852  dfom2  7870  relcnvexb  7929  dfsmo2  8340  ord1eln01  8487  ord2eln012  8488  omord  8559  nneob  8648  fsetcdmex  8866  pw2f1olem  9076  pwssfi  9168  sucdom  9211  1sdom  9222  fundmfibi  9300  f1dmvrnfibi  9305  fieq0  9388  hartogslem1  9511  rankr1ag  9781  rankeq0b  9839  fidomtri  9995  fidomtri2  9996  pr2ne  10005  isfin2-2  10318  enfin2i  10320  isfin3-2  10366  isf34lem6  10379  isfin1-2  10384  isfin1-3  10385  isfin7-2  10395  axgroth6  10830  ltsonq  10971  ltexnq  10977  znegclb  12648  rpneg  13068  nltpnft  13208  ngtmnft  13210  xrrebnd  13212  qextlt  13247  qextle  13248  iccneg  13517  fzsn  13613  fz1sbc  13647  fzdif1  13652  fzofzp1b  13813  ceilidz  13905  fleqceilz  13907  hashclb  14414  hashnncl  14422  hashfun  14494  reim0b  15196  rexanre  15424  rexuzre  15430  lo1resb  15641  o1resb  15643  dvdsext  16403  zob  16441  ncoprmgcdne1b  16732  pceq0  16955  pc11  16964  pcz  16965  ramtcl  17094  cshwsiun  17183  oduposb  18407  pospo  18423  cnvpsb  18659  tsrlemax  18666  issubg2  19254  issubg4  19258  eqg0subg  19313  ghmmhmb  19343  pmtrmvd  19572  mndodcong  19658  issubrng2  20709  issubrg2  20743  isdrng5  20906  ring2idlqusb  21502  lpigen  21555  cyggic  21774  ip2eq  21855  maducoeval2  22849  eltg3  23171  bastop  23190  0top  23192  iscld3  23273  isclo2  23297  cnprest  23498  dfconn2  23628  comppfsc  23742  cmphaushmeo  24010  reghaus  24035  nrmhaus  24036  fbun  24050  fsubbas  24077  ufileu  24129  uffix  24131  txflf  24216  fclsrest  24234  flimfnfcls  24238  ptcmplem2  24263  tgpt1  24328  tgpt0  24329  isngp2  24807  nrgdomn  24881  nmhmcn  25332  iscmet3  25505  limcflf  26093  ply1nzb  26333  coe11  26463  dgreq0  26475  eldmgm  27239  sqf11  27356  sqff1o  27399  zabsle1  27513  lgsabs1  27553  lgsquadlem2  27598  madebday  28146  oldbday  28147  leslss  28155  oldfib  28623  z12negsclb  28727  bdayfin  28733  issubgr2  29682  uhgrissubgr  29685  usgrfilem  29737  uvtxnbgrb  29811  nbusgrvtxm1uvtx  29815  cusgrfilem3  29867  vdiscusgr  29941  wwlksn0s  30279  clwwlknon1loop  30518  clwwlknun  30532  nmobndi  31200  hmopadj2  32366  mdslle1i  32742  mdslle2i  32743  relfi  33020  ssrelf  33033  prodindf  33254  bnj1173  35457  r1filim  35558  revwlkb  35668  resconn  35777  cvmsval  35797  fmlafvel  35916  dmopab3rexdif  35936  elmrsubrn  36051  funsseq  36299  brcolinear  36590  outsideofeu  36662  lineunray  36678  nn0prpw  36893  ttcsnexbig  37091  bj-nfimexal  37290  bj-spvw  37316  bj-sngltag  37678  bj-elpwg  37747  bj-elsn0  37858  bj-opelid  37859  bj-opelidres  37864  bj-ideqg1  37867  bj-imdirval3  37887  bj-inftyexpiinj  37912  qdiff  38030  poimirlem26  38356  poimirlem27  38357  heicant  38365  cover2  38426  isbndx  38493  isbnd2  38494  equivbnd2  38503  prdsbnd2  38506  elghomlem2OLD  38597  isdrngo3  38670  riotaclbgBAD  39788  lssatle  39849  opcon3b  40030  cdlemk33N  41743  cdlemk34  41744  quadfac  43032  ioin9i8  43036  eu6w  43468  wepwsolem  43829  onsupmaxb  44026  rp-fakeimass  44298  iscard5  44322  cnvssb  44372  intimag  44442  ntrneiiso  44877  pm11.71  45167  pm14.122b  45193  pm14.123b  45196  iotavalb  45200  relwf  45736  elixpconstg  45867  eliuniin  45877  eliuniin2  45898  climreeq  46389  f1cof1b  47874  rexrsb  47897  afv0nbfvbi  47948  dfafn5b  47958  elfz2z  48112  zeo2ALTV  48496  fpprwpprb  48565  dfsclnbgr6  48683  nnlog2ge0lt1  49405  oppccatb  49853