Theorem impbid1 228

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 215	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  impbid2  229  iba  536  pm5.61  1016  pm5.71  1043  cad0  1645  19.33b  1912  19.40b  1915  19.9t  2246  axc16gb  2304  equs5  2498  2eu1  2684  2eu1v  2685  2eu3  2687  ceqsalgALT  3499  eqvincg  3616  reuxfrd  3720  2reu1  3859  disjeq0  4422  undif4  4433  iftrueb  4505  ssprsseq  4795  sneqbg  4812  preq1b  4815  opthpr  4820  preq12nebg  4832  opthprneg  4834  dfiun2g  4998  elpwuni  5075  disjxiun  5110  eusv2i  5366  reusv2lem3  5372  reusv3  5377  soltmin  6137  ssxpb  6173  xp11  6174  xpcan  6175  xpcan2  6176  ordssun  6466  suc11  6471  unizlim  6486  imadif  6621  2elresin  6657  mpteqb  7010  f1fveq  7261  f1elima  7262  f1imass  7263  fliftf  7314  funeldmb  7358  sorpssuni  7730  sorpssint  7731  iunpw  7770  ssonprc  7786  onint0  7790  oa00  8544  omcan  8554  omopth2  8569  oecan  8575  nnarcl  8602  iserd  8721  mapfset  8847  map0g  8882  fundmen  9028  fopwdom  9073  onfin  9199  0sdom1dom  9206  fineqvlem  9226  f1finf1o  9233  isfiniteg  9260  inficl  9385  tc00  9715  cardnueq0  9950  cardsdomel  9960  wdomfil  10045  wdomnumr  10048  alephsucdom  10063  cardalephex  10074  dfac12lem2  10128  cfeq0  10240  fin23lem24  10306  fin1a2lem9  10392  carden  10535  axrepnd  10579  axacndlem4  10595  gchpwdom  10655  gchina  10684  r1tskina  10767  addcanpi  10884  mulcanpi  10885  elnpi  10973  addcan  11394  addcan2  11395  neg11  11509  negreb  11523  add20  11726  mulcand  11847  cru  12210  nn0lt10b  12658  uz11  12887  eqreznegel  12958  lbzbi  12960  rpnnen1lem6  13006  xrmaxlt  13207  xrltmin  13208  xrmaxle  13209  xrlemin  13210  xneg11  13241  xnn0xadd0  13273  xsubge0  13287  xrub  13338  elioc2  13436  elico2  13437  elicc2  13438  fzopth  13589  2ffzeq  13677  fzoopth  13791  flidz  13843  addmodlteq  13982  expeq0  14128  sq01  14261  fz1eqb  14390  hashen1  14406  hash1snb  14456  hashle2pr  14514  wrdnval  14582  eqwrd  14594  ccatalpha  14631  wrdl1s1  14652  ccats1alpha  14657  ccatopth  14753  ccatopth2  14754  wrdlen2  14981  cj11  15213  sqrt0  15292  abs00  15340  recan  15388  cnsqrt00  15444  rlimdm  15602  rpnnen2lem12  16281  0dvds  16334  dvds1  16377  alzdvds  16378  nn0enne  16435  nn0oddm1d2  16443  nnoddm1d2  16444  gcdeq0  16575  algcvgblem  16635  2mulprm  16751  prmexpb  16778  prmreclem3  16978  4sqlem11  17015  moni  17793  chnfibg  18692  grprcan  19040  grplcan  19067  grpinv11  19074  galcan  19374  sylow2a  19689  subgdisjb  19763  0ringdif  20611  domnlcanb  20804  domnrcanb  20806  drngmuleq0  20845  fidomndrng  20855  lspsncmp  21218  xrsdsreclb  21533  znidomb  21680  lmisfree  21961  coe1tm  22403  tgdom  23104  en1top  23110  cmpfi  23534  txcmpb  23770  hmeocnvb  23900  flimcls  24111  hauspwpwf1  24113  flftg  24122  ghmcnp  24241  metrest  24650  icoopnst  25067  iocopnst  25068  ishl2  25498  vitali  25741  mbfi1fseqlem4  25846  aannenlem1  26458  perfect  27361  2lgsoddprmlem3  27544  2sq2  27563  ltsval2  27786  bday0b  27972  negs11  28208  elnns2  28500  n0cutlt  28518  umgrislfupgrlem  29413  usgrausgrb  29460  upgriswlk  29931  uhgrwkspth  30045  usgr2wlkspth  30049  usgr2trlspth  30051  usgr2pthspth  30052  extwwlkfab  30644  grporcan  30811  grpolcan  30823  ip2eqi  31149  hial2eq  31399  eigorthi  32130  stge1i  32531  stle0i  32532  mdbr3  32590  mdbr4  32591  atsseq  32640  mdsymlem7  32702  reuxfrdf  32778  disjunsn  32880  fpwrelmapffslem  33018  xmulcand  33181  prsdm  34249  prsrn  34250  lfuhgr  35509  lfuhgr2  35510  mthmpps  35973  untangtr  36105  filnetlem4  36781  ordtopconn  36839  ordtopt0  36842  bj-dfbi6  37057  bj-spvew  37147  bj-19.9htbi  37217  bj-axseprep  37599  bj-elid6  37702  icorempo  37885  inunissunidif  37909  fvineqsneu  37945  wl-lem-moexsb  38111  seqpo  38286  qmapeldisjsbi  39400  lshpcmp  39652  lsatcmp  39667  lsatcmp2  39668  ltrneq2  40812  ltrneq  40813  tendospcanN  41687  dochlkr  42049  lcfl7N  42165  hgmap11  42566  ccatcan2d  42909  remulcan2d  42914  itrere  42969  log11d  42997  resubcan2  43039  readdcan2  43064  sn-addcand  43071  sn-addcan2d  43073  remulcand  43090  sn-itrere  43152  sn-retire  43153  cnreeu  43154  fphpd  43435  pellexlem3  43450  qirropth  43527  expdioph  43642  rpnnen3  43651  iotasbc  45021  f1ocof1ob2  47708  2reu3  47736  rlimdmafv  47803  afv2orxorb  47854  rlimdmafv2  47884  funop1  47909  2ffzoeq  47954  prprelprb  48155  poprelb  48162  evenprm2  48368  perfectALTV  48377  nnsum3primesle9  48448  upgrwlkupwlkb  48795  islinindfis  49114  lincresunit3lem3  49139  blen1b  49253  line2ylem  49416  line2y  49420  intubeu  49647  unilbeu  49648  thincn0eu  50094