Theorem impbid2 225

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  biimt  360  bimsc1  842  biorf  935  pm4.72  948  19.38a  1842  19.38b  1843  ax13b  2035  19.3t  2194  cgsexg  3518  cgsex2g  3519  cgsex4g  3520  cgsex4gOLD  3521  cgsex4gOLDOLD  3522  elab3gf  3674  elab3g  3675  abidnf  3698  reuan  3890  sscon34b  4294  elsn2g  4666  eqoreldif  4688  difsn  4801  elpreqprb  4868  dfnfc2  4933  intmin4  4981  dfiin2g  5035  elpw2g  5344  ssrel  5782  ssrelOLD  5783  ssrel2  5785  ssrelrel  5796  dmopab2rex  5917  releldmb  5945  relelrnb  5946  cnveqb  6195  dmsnopg  6212  relcnvtrg  6265  elsnxp  6290  onelssex  6412  ord0eln0  6419  f1ocnvb  6846  eqfnun  7038  ffvresb  7126  isof1oopb  7324  soisores  7326  riotaclb  7409  fnoprabg  7533  difex2  7749  dfwe2  7763  ordpwsuc  7805  ordunisuc2  7835  limsssuc  7841  dfom2  7859  relcnvexb  7919  dfsmo2  8349  ord1eln01  8498  ord2eln012  8499  omord  8570  nneob  8657  fsetcdmex  8859  pw2f1olem  9078  sucdom  9237  sucdomOLD  9238  1sdom  9250  fundmfibi  9333  f1dmvrnfibi  9338  fieq0  9418  hartogslem1  9539  rankr1ag  9799  rankeq0b  9857  fidomtri  9990  fidomtri2  9991  pr2ne  10001  isfin2-2  10316  enfin2i  10318  isfin3-2  10364  isf34lem6  10377  isfin1-2  10382  isfin1-3  10383  isfin7-2  10393  axgroth6  10825  ltsonq  10966  ltexnq  10972  znegclb  12603  rpneg  13010  nltpnft  13147  ngtmnft  13149  xrrebnd  13151  qextlt  13186  qextle  13187  iccneg  13453  fzsn  13547  fz1sbc  13581  fzofzp1b  13734  ceilidz  13821  fleqceilz  13823  hashclb  14322  hashnncl  14330  hashfun  14401  reim0b  15070  rexanre  15297  rexuzre  15303  lo1resb  15512  o1resb  15514  dvdsext  16268  zob  16306  ncoprmgcdne1b  16591  pceq0  16808  pc11  16817  pcz  16818  ramtcl  16947  cshwsiun  17037  oduposb  18286  pospo  18302  cnvpsb  18536  tsrlemax  18543  issubg2  19057  issubg4  19061  eqg0subg  19111  ghmmhmb  19141  pmtrmvd  19365  mndodcong  19451  issubrng2  20446  issubrg2  20482  ring2idlqusb  21069  lpigen  21094  cyggic  21347  ip2eq  21425  maducoeval2  22362  eltg3  22685  bastop  22704  0top  22706  iscld3  22788  isclo2  22812  cnprest  23013  dfconn2  23143  comppfsc  23256  cmphaushmeo  23524  reghaus  23549  nrmhaus  23550  fbun  23564  fsubbas  23591  ufileu  23643  uffix  23645  txflf  23730  fclsrest  23748  flimfnfcls  23752  ptcmplem2  23777  tgpt1  23842  tgpt0  23843  isngp2  24326  nrgdomn  24408  nmhmcn  24860  iscmet3  25034  limcflf  25622  ply1nzb  25864  coe11  25991  dgreq0  26003  eldmgm  26750  sqf11  26867  sqff1o  26910  zabsle1  27023  lgsabs1  27063  lgsquadlem2  27108  madebday  27619  oldbday  27620  slelss  27627  issubgr2  28784  uhgrissubgr  28787  usgrfilem  28839  uvtxnbgrb  28913  nbusgrvtxm1uvtx  28917  cusgrfilem3  28969  vdiscusgr  29043  wwlksn0s  29370  clwwlknon1loop  29606  clwwlknun  29620  nmobndi  30283  hmopadj2  31449  mdslle1i  31825  mdslle2i  31826  relfi  32088  ssrelf  32099  prodindf  33307  bnj1173  34299  revwlkb  34402  resconn  34523  cvmsval  34543  fmlafvel  34662  dmopab3rexdif  34682  elmrsubrn  34797  funsseq  35031  brcolinear  35323  outsideofeu  35395  lineunray  35411  nn0prpw  35511  bj-nfimexal  35806  bj-sngltag  36167  bj-elpwg  36236  bj-elsn0  36339  bj-opelid  36340  bj-opelidres  36345  bj-ideqg1  36348  bj-imdirval3  36368  bj-inftyexpiinj  36393  wl-ax11-lem2  36751  poimirlem26  36817  poimirlem27  36818  heicant  36826  cover2  36886  isbndx  36953  isbnd2  36954  equivbnd2  36963  prdsbnd2  36966  elghomlem2OLD  37057  isdrngo3  37130  riotaclbgBAD  38127  lssatle  38188  opcon3b  38369  cdlemk33N  40083  cdlemk34  40084  ioin9i8  41330  wepwsolem  42086  onsupmaxb  42290  rp-fakeimass  42565  iscard5  42589  cnvssb  42639  intimag  42709  ntrneiiso  43144  pm11.71  43458  pm14.122b  43484  pm14.123b  43487  iotavalb  43491  elixpconstg  44080  eliuniin  44090  eliuniin2  44111  climreeq  44628  f1cof1b  46084  rexrsb  46107  afv0nbfvbi  46158  dfafn5b  46168  elfz2z  46322  zeo2ALTV  46638  fpprwpprb  46707  nnlog2ge0lt1  47340