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  3492  cgsex2g  3493  cgsex4g  3494  cgsex4gOLD  3495  elab3gf  3651  elab3g  3652  abidnf  3673  reuan  3859  sscon34b  4267  elsn2g  4628  eqoreldif  4649  difsn  4762  elpreqprb  4832  dfnfc2  4893  intmin4  4941  dfiin2g  4996  elpw2g  5288  ssrel  5745  ssrelOLD  5746  ssrel2  5748  ssrelrel  5759  dmopab2rex  5881  releldmb  5910  relelrnb  5911  cnveqb  6169  dmsnopg  6186  relcnvtrg  6239  elsnxp  6264  onelssex  6381  ord0eln0  6388  f1ocnvb  6813  eqfnun  7009  ffvresb  7097  isof1oopb  7300  soisores  7302  riotaclb  7385  fnoprabg  7512  difex2  7736  dfwe2  7750  ordpwsuc  7790  ordunisuc2  7820  limsssuc  7826  dfom2  7844  relcnvexb  7902  dfsmo2  8316  ord1eln01  8460  ord2eln012  8461  omord  8532  nneob  8620  fsetcdmex  8836  pw2f1olem  9045  pwssfi  9141  sucdom  9183  1sdom  9195  fundmfibi  9287  f1dmvrnfibi  9292  fieq0  9372  hartogslem1  9495  rankr1ag  9755  rankeq0b  9813  fidomtri  9946  fidomtri2  9947  pr2ne  9957  isfin2-2  10272  enfin2i  10274  isfin3-2  10320  isf34lem6  10333  isfin1-2  10338  isfin1-3  10339  isfin7-2  10349  axgroth6  10781  ltsonq  10922  ltexnq  10928  znegclb  12570  rpneg  12985  nltpnft  13124  ngtmnft  13126  xrrebnd  13128  qextlt  13163  qextle  13164  iccneg  13433  fzsn  13527  fz1sbc  13561  fzdif1  13566  fzofzp1b  13726  ceilidz  13814  fleqceilz  13816  hashclb  14323  hashnncl  14331  hashfun  14402  reim0b  15085  rexanre  15313  rexuzre  15319  lo1resb  15530  o1resb  15532  dvdsext  16291  zob  16329  ncoprmgcdne1b  16620  pceq0  16842  pc11  16851  pcz  16852  ramtcl  16981  cshwsiun  17070  oduposb  18288  pospo  18304  cnvpsb  18538  tsrlemax  18545  issubg2  19073  issubg4  19077  eqg0subg  19128  ghmmhmb  19159  pmtrmvd  19386  mndodcong  19472  issubrng2  20467  issubrg2  20501  ring2idlqusb  21220  lpigen  21245  cyggic  21482  ip2eq  21562  maducoeval2  22527  eltg3  22849  bastop  22868  0top  22870  iscld3  22951  isclo2  22975  cnprest  23176  dfconn2  23306  comppfsc  23419  cmphaushmeo  23687  reghaus  23712  nrmhaus  23713  fbun  23727  fsubbas  23754  ufileu  23806  uffix  23808  txflf  23893  fclsrest  23911  flimfnfcls  23915  ptcmplem2  23940  tgpt1  24005  tgpt0  24006  isngp2  24485  nrgdomn  24559  nmhmcn  25020  iscmet3  25193  limcflf  25782  ply1nzb  26028  coe11  26158  dgreq0  26171  eldmgm  26932  sqf11  27049  sqff1o  27092  zabsle1  27207  lgsabs1  27247  lgsquadlem2  27292  madebday  27811  oldbday  27812  slelss  27820  zs12negsclb  28341  issubgr2  29199  uhgrissubgr  29202  usgrfilem  29254  uvtxnbgrb  29328  nbusgrvtxm1uvtx  29332  cusgrfilem3  29385  vdiscusgr  29459  wwlksn0s  29791  clwwlknon1loop  30027  clwwlknun  30041  nmobndi  30704  hmopadj2  31870  mdslle1i  32246  mdslle2i  32247  relfi  32531  ssrelf  32543  prodindf  32786  bnj1173  34992  revwlkb  35113  resconn  35233  cvmsval  35253  fmlafvel  35372  dmopab3rexdif  35392  elmrsubrn  35507  funsseq  35755  brcolinear  36047  outsideofeu  36119  lineunray  36135  nn0prpw  36311  bj-nfimexal  36614  bj-sngltag  36971  bj-elpwg  37040  bj-elsn0  37143  bj-opelid  37144  bj-opelidres  37149  bj-ideqg1  37152  bj-imdirval3  37172  bj-inftyexpiinj  37197  wl-ax11-lem2  37574  poimirlem26  37640  poimirlem27  37641  heicant  37649  cover2  37709  isbndx  37776  isbnd2  37777  equivbnd2  37786  prdsbnd2  37789  elghomlem2OLD  37880  isdrngo3  37953  riotaclbgBAD  38947  lssatle  39008  opcon3b  39189  cdlemk33N  40903  cdlemk34  40904  ioin9i8  42195  eu6w  42664  wepwsolem  43031  onsupmaxb  43228  rp-fakeimass  43501  iscard5  43525  cnvssb  43575  intimag  43645  ntrneiiso  44080  pm11.71  44386  pm14.122b  44412  pm14.123b  44415  iotavalb  44419  relwf  44957  elixpconstg  45083  eliuniin  45093  eliuniin2  45114  climreeq  45611  f1cof1b  47078  rexrsb  47101  afv0nbfvbi  47152  dfafn5b  47162  elfz2z  47316  zeo2ALTV  47672  fpprwpprb  47741  dfsclnbgr6  47858  nnlog2ge0lt1  48555  oppccatb  49005