Theorem impbid1 224

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 211	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:  impbid2  225  iba  527  pm5.61  997  pm5.71  1024  cad0  1621  cad0OLD  1622  19.33b  1889  19.40b  1892  19.9t  2200  axc16gb  2257  equs5  2460  2eu1  2652  2eu1v  2653  2eu3  2655  ceqsalgALT  3455  eqvincg  3570  reuxfrd  3678  2reu1  3826  disjeq0  4386  undif4  4397  ssprsseq  4755  sneqbg  4771  preq1b  4774  opthpr  4779  preq12nebg  4790  opthprneg  4792  elpwuni  5030  disjxiun  5067  eusv2i  5312  reusv2lem3  5318  reusv3  5323  soltmin  6030  ssxpb  6066  xp11  6067  xpcan  6068  xpcan2  6069  ordssun  6350  suc11  6354  unizlim  6368  imadif  6502  2elresin  6537  mpteqb  6876  f1fveq  7116  f1elima  7117  f1imass  7118  fliftf  7166  sorpssuni  7563  sorpssint  7564  iunpw  7599  ssonprc  7614  onint0  7618  oa00  8352  omcan  8362  omopth2  8377  oecan  8382  nnarcl  8409  iserd  8482  mapfset  8596  map0g  8630  fundmen  8775  fopwdom  8820  onfin  8944  fineqvlem  8966  f1finf1o  8975  isfiniteg  9004  inficl  9114  tc00  9437  cardnueq0  9653  cardsdomel  9663  wdomfil  9748  wdomnumr  9751  alephsucdom  9766  cardalephex  9777  dfac12lem2  9831  cfeq0  9943  fin23lem24  10009  fin1a2lem9  10095  carden  10238  axrepnd  10281  axacndlem4  10297  gchpwdom  10357  gchina  10386  r1tskina  10469  addcanpi  10586  mulcanpi  10587  elnpi  10675  addcan  11089  addcan2  11090  neg11  11202  negreb  11216  add20  11417  mulcand  11538  cru  11895  nn0lt10b  12312  uz11  12536  eqreznegel  12603  lbzbi  12605  rpnnen1lem6  12651  xrmaxlt  12844  xrltmin  12845  xrmaxle  12846  xrlemin  12847  xneg11  12878  xnn0xadd0  12910  xsubge0  12924  xrub  12975  elioc2  13071  elico2  13072  elicc2  13073  fzopth  13222  2ffzeq  13306  flidz  13458  addmodlteq  13594  expeq0  13741  sq01  13868  fz1eqb  13997  hashen1  14013  hash1snb  14062  hashle2pr  14119  wrdnval  14176  eqwrd  14188  ccatalpha  14226  wrdl1s1  14247  ccats1alpha  14252  ccatopth  14357  ccatopth2  14358  wrdlen2  14585  cj11  14801  sqrt0  14881  abs00  14929  recan  14976  cnsqrt00  15032  rlimdm  15188  rpnnen2lem12  15862  0dvds  15914  dvds1  15956  alzdvds  15957  nn0enne  16014  nn0oddm1d2  16022  nnoddm1d2  16023  gcdeq0  16152  algcvgblem  16210  2mulprm  16326  prmexpb  16353  prmreclem3  16547  4sqlem11  16584  moni  17365  grprcan  18528  grplcan  18552  grpinv11  18559  galcan  18825  sylow2a  19139  subgdisjb  19214  drngmuleq0  19929  lspsncmp  20293  fidomndrng  20492  xrsdsreclb  20557  znidomb  20681  lmisfree  20959  coe1tm  21354  tgdom  22036  en1top  22042  cmpfi  22467  txcmpb  22703  hmeocnvb  22833  flimcls  23044  hauspwpwf1  23046  flftg  23055  ghmcnp  23174  metrest  23586  icoopnst  24008  iocopnst  24009  ishl2  24439  vitali  24682  mbfi1fseqlem4  24788  aannenlem1  25393  perfect  26284  2lgsoddprmlem3  26467  2sq2  26486  umgrislfupgrlem  27395  usgrausgrb  27442  upgriswlk  27910  uhgrwkspth  28024  usgr2wlkspth  28028  usgr2trlspth  28030  usgr2pthspth  28031  extwwlkfab  28617  grporcan  28781  grpolcan  28793  ip2eqi  29119  hial2eq  29369  eigorthi  30100  stge1i  30501  stle0i  30502  mdbr3  30560  mdbr4  30561  atsseq  30610  mdsymlem7  30672  reuxfrdf  30740  disjunsn  30834  fpwrelmapffslem  30969  xmulcand  31097  prsdm  31766  prsrn  31767  lfuhgr  32979  lfuhgr2  32980  mthmpps  33444  untangtr  33555  funeldmb  33643  sltval2  33786  bday0b  33951  filnetlem4  34497  ordtopconn  34555  ordtopt0  34558  bj-dfbi6  34683  bj-19.9htbi  34812  bj-elid6  35268  icorempo  35449  inunissunidif  35473  fvineqsneu  35509  wl-lem-moexsb  35650  seqpo  35832  lshpcmp  36929  lsatcmp  36944  lsatcmp2  36945  ltrneq2  38089  ltrneq  38090  tendospcanN  38964  dochlkr  39326  lcfl7N  39442  hgmap11  39843  ccatcan2d  40145  remulcan2d  40214  resubcan2  40292  readdcan2  40316  sn-addcand  40322  sn-addcan2d  40324  remulcand  40341  itrere  40357  retire  40358  cnreeu  40359  fphpd  40554  pellexlem3  40569  qirropth  40646  expdioph  40761  rpnnen3  40770  iotasbc  41926  f1ocof1ob2  44461  2reu3  44489  rlimdmafv  44556  afv2orxorb  44607  rlimdmafv2  44637  funop1  44662  fzoopth  44707  2ffzoeq  44708  prprelprb  44857  poprelb  44864  evenprm2  45054  perfectALTV  45063  nnsum3primesle9  45134  upgrwlkupwlkb  45191  0ringdif  45316  islinindfis  45678  lincresunit3lem3  45703  blen1b  45822  line2ylem  45985  line2y  45989  intubeu  46158  unilbeu  46159  thincn0eu  46201