Theorem impbid1 225

Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.)

Hypotheses

Ref	Expression
impbid1.1	⊢ (𝜑 → (𝜓 → 𝜒))
impbid1.2	⊢ (𝜒 → 𝜓)

Assertion

Ref	Expression
impbid1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem impbid1

Step	Hyp	Ref	Expression
1		impbid1.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		impbid1.2	. . 3 ⊢ (𝜒 → 𝜓)
3	2	a1i 11	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	impbid 212	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:  impbid2  226  iba  527  pm5.61  1002  pm5.71  1029  cad0  1614  19.33b  1882  19.40b  1885  19.9t  2201  axc16gb  2259  equs5  2462  2eu1  2648  2eu1v  2649  2eu3  2651  ceqsalgALT  3515  eqvincg  3647  reuxfrd  3756  2reu1  3905  disjeq0  4461  undif4  4472  ssprsseq  4829  sneqbg  4847  preq1b  4850  opthpr  4855  preq12nebg  4867  opthprneg  4869  dfiun2g  5034  elpwuni  5109  disjxiun  5144  eusv2i  5399  reusv2lem3  5405  reusv3  5410  soltmin  6158  ssxpb  6195  xp11  6196  xpcan  6197  xpcan2  6198  ordssun  6487  suc11  6492  unizlim  6508  imadif  6651  2elresin  6689  mpteqb  7034  f1fveq  7281  f1elima  7282  f1imass  7283  fliftf  7334  funeldmb  7378  sorpssuni  7750  sorpssint  7751  iunpw  7789  ssonprc  7806  onint0  7810  oa00  8595  omcan  8605  omopth2  8620  oecan  8625  nnarcl  8652  iserd  8769  mapfset  8888  map0g  8922  fundmen  9069  fopwdom  9118  onfin  9264  0sdom1dom  9271  fineqvlem  9295  f1finf1o  9302  f1finf1oOLD  9303  isfiniteg  9334  inficl  9462  tc00  9785  cardnueq0  10001  cardsdomel  10011  wdomfil  10098  wdomnumr  10101  alephsucdom  10116  cardalephex  10127  dfac12lem2  10182  cfeq0  10293  fin23lem24  10359  fin1a2lem9  10445  carden  10588  axrepnd  10631  axacndlem4  10647  gchpwdom  10707  gchina  10736  r1tskina  10819  addcanpi  10936  mulcanpi  10937  elnpi  11025  addcan  11442  addcan2  11443  neg11  11557  negreb  11571  add20  11772  mulcand  11893  cru  12255  nn0lt10b  12677  uz11  12900  eqreznegel  12973  lbzbi  12975  rpnnen1lem6  13021  xrmaxlt  13219  xrltmin  13220  xrmaxle  13221  xrlemin  13222  xneg11  13253  xnn0xadd0  13285  xsubge0  13299  xrub  13350  elioc2  13446  elico2  13447  elicc2  13448  fzopth  13597  2ffzeq  13685  fzoopth  13797  flidz  13846  addmodlteq  13983  expeq0  14129  sq01  14260  fz1eqb  14389  hashen1  14405  hash1snb  14454  hashle2pr  14512  wrdnval  14579  eqwrd  14591  ccatalpha  14627  wrdl1s1  14648  ccats1alpha  14653  ccatopth  14750  ccatopth2  14751  wrdlen2  14979  cj11  15197  sqrt0  15276  abs00  15324  recan  15371  cnsqrt00  15427  rlimdm  15583  rpnnen2lem12  16257  0dvds  16310  dvds1  16352  alzdvds  16353  nn0enne  16410  nn0oddm1d2  16418  nnoddm1d2  16419  gcdeq0  16550  algcvgblem  16610  2mulprm  16726  prmexpb  16752  prmreclem3  16951  4sqlem11  16988  moni  17783  grprcan  19003  grplcan  19030  grpinv11  19037  grpinv11OLD  19038  galcan  19334  sylow2a  19651  subgdisjb  19725  0ringdif  20543  domnlcanb  20736  domnrcanb  20738  drngmuleq0  20779  fidomndrng  20790  lspsncmp  21135  xrsdsreclb  21448  znidomb  21597  lmisfree  21879  coe1tm  22291  tgdom  23000  en1top  23006  cmpfi  23431  txcmpb  23667  hmeocnvb  23797  flimcls  24008  hauspwpwf1  24010  flftg  24019  ghmcnp  24138  metrest  24552  icoopnst  24982  iocopnst  24983  ishl2  25417  vitali  25661  mbfi1fseqlem4  25767  aannenlem1  26384  perfect  27289  2lgsoddprmlem3  27472  2sq2  27491  sltval2  27715  bday0b  27889  negs11  28095  elnns2  28358  umgrislfupgrlem  29153  usgrausgrb  29200  upgriswlk  29673  uhgrwkspth  29787  usgr2wlkspth  29791  usgr2trlspth  29793  usgr2pthspth  29794  extwwlkfab  30380  grporcan  30546  grpolcan  30558  ip2eqi  30884  hial2eq  31134  eigorthi  31865  stge1i  32266  stle0i  32267  mdbr3  32325  mdbr4  32326  atsseq  32375  mdsymlem7  32437  reuxfrdf  32518  disjunsn  32613  fpwrelmapffslem  32749  xmulcand  32887  prsdm  33874  prsrn  33875  lfuhgr  35101  lfuhgr2  35102  mthmpps  35566  untangtr  35693  filnetlem4  36363  ordtopconn  36421  ordtopt0  36424  bj-dfbi6  36557  bj-19.9htbi  36685  bj-elid6  37152  icorempo  37333  inunissunidif  37357  fvineqsneu  37393  wl-lem-moexsb  37548  seqpo  37733  lshpcmp  38969  lsatcmp  38984  lsatcmp2  38985  ltrneq2  40130  ltrneq  40131  tendospcanN  41005  dochlkr  41367  lcfl7N  41483  hgmap11  41884  ccatcan2d  42270  remulcan2d  42276  itrere  42331  log11d  42360  resubcan2  42394  readdcan2  42418  sn-addcand  42425  sn-addcan2d  42427  remulcand  42444  sn-itrere  42474  sn-retire  42475  cnreeu  42476  fphpd  42803  pellexlem3  42818  qirropth  42895  expdioph  43011  rpnnen3  43020  iotasbc  44414  f1ocof1ob2  47031  2reu3  47059  rlimdmafv  47126  afv2orxorb  47177  rlimdmafv2  47207  funop1  47232  2ffzoeq  47276  prprelprb  47441  poprelb  47448  evenprm2  47638  perfectALTV  47647  nnsum3primesle9  47718  upgrwlkupwlkb  47984  islinindfis  48294  lincresunit3lem3  48319  blen1b  48437  line2ylem  48600  line2y  48604  intubeu  48772  unilbeu  48773  thincn0eu  48831