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  1619  19.33b  1886  19.40b  1889  19.9t  2207  axc16gb  2265  equs5  2460  2eu1  2646  2eu1v  2647  2eu3  2649  ceqsalgALT  3473  eqvincg  3598  reuxfrd  3702  2reu1  3843  disjeq0  4405  undif4  4416  iftrueb  4487  ssprsseq  4776  sneqbg  4794  preq1b  4797  opthpr  4802  preq12nebg  4814  opthprneg  4816  dfiun2g  4980  elpwuni  5055  disjxiun  5090  eusv2i  5334  reusv2lem3  5340  reusv3  5345  soltmin  6088  ssxpb  6127  xp11  6128  xpcan  6129  xpcan2  6130  ordssun  6416  suc11  6421  unizlim  6436  imadif  6571  2elresin  6608  mpteqb  6954  f1fveq  7202  f1elima  7203  f1imass  7204  fliftf  7255  funeldmb  7299  sorpssuni  7671  sorpssint  7672  iunpw  7710  ssonprc  7726  onint0  7730  oa00  8480  omcan  8490  omopth2  8505  oecan  8510  nnarcl  8537  iserd  8654  mapfset  8780  map0g  8814  fundmen  8959  fopwdom  9004  onfin  9130  0sdom1dom  9136  fineqvlem  9156  f1finf1o  9163  isfiniteg  9190  inficl  9315  tc00  9642  cardnueq0  9863  cardsdomel  9873  wdomfil  9958  wdomnumr  9961  alephsucdom  9976  cardalephex  9987  dfac12lem2  10042  cfeq0  10153  fin23lem24  10219  fin1a2lem9  10305  carden  10448  axrepnd  10491  axacndlem4  10507  gchpwdom  10567  gchina  10596  r1tskina  10679  addcanpi  10796  mulcanpi  10797  elnpi  10885  addcan  11303  addcan2  11304  neg11  11418  negreb  11432  add20  11635  mulcand  11756  cru  12123  nn0lt10b  12541  uz11  12763  eqreznegel  12838  lbzbi  12840  rpnnen1lem6  12886  xrmaxlt  13086  xrltmin  13087  xrmaxle  13088  xrlemin  13089  xneg11  13120  xnn0xadd0  13152  xsubge0  13166  xrub  13217  elioc2  13315  elico2  13316  elicc2  13317  fzopth  13467  2ffzeq  13555  fzoopth  13668  flidz  13720  addmodlteq  13859  expeq0  14005  sq01  14138  fz1eqb  14267  hashen1  14283  hash1snb  14332  hashle2pr  14390  wrdnval  14458  eqwrd  14470  ccatalpha  14507  wrdl1s1  14528  ccats1alpha  14533  ccatopth  14629  ccatopth2  14630  wrdlen2  14857  cj11  15075  sqrt0  15154  abs00  15202  recan  15250  cnsqrt00  15306  rlimdm  15464  rpnnen2lem12  16140  0dvds  16193  dvds1  16236  alzdvds  16237  nn0enne  16294  nn0oddm1d2  16302  nnoddm1d2  16303  gcdeq0  16434  algcvgblem  16494  2mulprm  16610  prmexpb  16636  prmreclem3  16836  4sqlem11  16873  moni  17649  chnfibg  18548  grprcan  18892  grplcan  18919  grpinv11  18926  grpinv11OLD  18927  galcan  19222  sylow2a  19537  subgdisjb  19611  0ringdif  20448  domnlcanb  20641  domnrcanb  20643  drngmuleq0  20684  fidomndrng  20694  lspsncmp  21059  xrsdsreclb  21356  znidomb  21504  lmisfree  21785  coe1tm  22193  tgdom  22899  en1top  22905  cmpfi  23329  txcmpb  23565  hmeocnvb  23695  flimcls  23906  hauspwpwf1  23908  flftg  23917  ghmcnp  24036  metrest  24445  icoopnst  24869  iocopnst  24870  ishl2  25303  vitali  25547  mbfi1fseqlem4  25652  aannenlem1  26269  perfect  27175  2lgsoddprmlem3  27358  2sq2  27377  sltval2  27601  bday0b  27780  negs11  27997  elnns2  28275  n0cutlt  28291  umgrislfupgrlem  29107  usgrausgrb  29154  upgriswlk  29626  uhgrwkspth  29740  usgr2wlkspth  29744  usgr2trlspth  29746  usgr2pthspth  29747  extwwlkfab  30339  grporcan  30505  grpolcan  30517  ip2eqi  30843  hial2eq  31093  eigorthi  31824  stge1i  32225  stle0i  32226  mdbr3  32284  mdbr4  32285  atsseq  32334  mdsymlem7  32396  reuxfrdf  32477  disjunsn  32581  fpwrelmapffslem  32722  xmulcand  32908  prsdm  33934  prsrn  33935  lfuhgr  35169  lfuhgr2  35170  mthmpps  35633  untangtr  35765  filnetlem4  36432  ordtopconn  36490  ordtopt0  36493  bj-dfbi6  36626  bj-19.9htbi  36754  bj-elid6  37221  icorempo  37402  inunissunidif  37426  fvineqsneu  37462  wl-lem-moexsb  37619  seqpo  37793  lshpcmp  39093  lsatcmp  39108  lsatcmp2  39109  ltrneq2  40253  ltrneq  40254  tendospcanN  41128  dochlkr  41490  lcfl7N  41606  hgmap11  42007  ccatcan2d  42350  remulcan2d  42356  itrere  42417  log11d  42445  resubcan2  42487  readdcan2  42512  sn-addcand  42519  sn-addcan2d  42521  remulcand  42538  sn-itrere  42587  sn-retire  42588  cnreeu  42589  fphpd  42914  pellexlem3  42929  qirropth  43006  expdioph  43121  rpnnen3  43130  iotasbc  44517  f1ocof1ob2  47187  2reu3  47215  rlimdmafv  47282  afv2orxorb  47333  rlimdmafv2  47363  funop1  47388  2ffzoeq  47432  prprelprb  47622  poprelb  47629  evenprm2  47819  perfectALTV  47828  nnsum3primesle9  47899  upgrwlkupwlkb  48246  islinindfis  48555  lincresunit3lem3  48580  blen1b  48694  line2ylem  48857  line2y  48861  intubeu  49089  unilbeu  49090  thincn0eu  49537