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  1003  pm5.71  1030  cad0  1620  19.33b  1887  19.40b  1890  19.9t  2212  axc16gb  2270  equs5  2465  2eu1  2652  2eu1v  2653  2eu3  2655  ceqsalgALT  3467  eqvincg  3591  reuxfrd  3695  2reu1  3836  disjeq0  4397  undif4  4408  iftrueb  4480  ssprsseq  4769  sneqbg  4787  preq1b  4790  opthpr  4795  preq12nebg  4807  opthprneg  4809  dfiun2g  4973  elpwuni  5048  disjxiun  5083  eusv2i  5332  reusv2lem3  5338  reusv3  5343  soltmin  6094  ssxpb  6133  xp11  6134  xpcan  6135  xpcan2  6136  ordssun  6422  suc11  6427  unizlim  6442  imadif  6577  2elresin  6614  mpteqb  6962  f1fveq  7211  f1elima  7212  f1imass  7213  fliftf  7264  funeldmb  7308  sorpssuni  7680  sorpssint  7681  iunpw  7719  ssonprc  7735  onint0  7739  oa00  8488  omcan  8498  omopth2  8513  oecan  8519  nnarcl  8546  iserd  8664  mapfset  8791  map0g  8826  fundmen  8972  fopwdom  9017  onfin  9143  0sdom1dom  9150  fineqvlem  9170  f1finf1o  9177  isfiniteg  9204  inficl  9332  tc00  9661  cardnueq0  9882  cardsdomel  9892  wdomfil  9977  wdomnumr  9980  alephsucdom  9995  cardalephex  10006  dfac12lem2  10061  cfeq0  10172  fin23lem24  10238  fin1a2lem9  10324  carden  10467  axrepnd  10511  axacndlem4  10527  gchpwdom  10587  gchina  10616  r1tskina  10699  addcanpi  10816  mulcanpi  10817  elnpi  10905  addcan  11324  addcan2  11325  neg11  11439  negreb  11453  add20  11656  mulcand  11777  cru  12145  nn0lt10b  12585  uz11  12807  eqreznegel  12878  lbzbi  12880  rpnnen1lem6  12926  xrmaxlt  13127  xrltmin  13128  xrmaxle  13129  xrlemin  13130  xneg11  13161  xnn0xadd0  13193  xsubge0  13207  xrub  13258  elioc2  13356  elico2  13357  elicc2  13358  fzopth  13509  2ffzeq  13597  fzoopth  13711  flidz  13763  addmodlteq  13902  expeq0  14048  sq01  14181  fz1eqb  14310  hashen1  14326  hash1snb  14375  hashle2pr  14433  wrdnval  14501  eqwrd  14513  ccatalpha  14550  wrdl1s1  14571  ccats1alpha  14576  ccatopth  14672  ccatopth2  14673  wrdlen2  14900  cj11  15118  sqrt0  15197  abs00  15245  recan  15293  cnsqrt00  15349  rlimdm  15507  rpnnen2lem12  16186  0dvds  16239  dvds1  16282  alzdvds  16283  nn0enne  16340  nn0oddm1d2  16348  nnoddm1d2  16349  gcdeq0  16480  algcvgblem  16540  2mulprm  16656  prmexpb  16683  prmreclem3  16883  4sqlem11  16920  moni  17697  chnfibg  18596  grprcan  18943  grplcan  18970  grpinv11  18977  grpinv11OLD  18978  galcan  19273  sylow2a  19588  subgdisjb  19662  0ringdif  20498  domnlcanb  20691  domnrcanb  20693  drngmuleq0  20734  fidomndrng  20744  lspsncmp  21109  xrsdsreclb  21406  znidomb  21554  lmisfree  21835  coe1tm  22251  tgdom  22956  en1top  22962  cmpfi  23386  txcmpb  23622  hmeocnvb  23752  flimcls  23963  hauspwpwf1  23965  flftg  23974  ghmcnp  24093  metrest  24502  icoopnst  24919  iocopnst  24920  ishl2  25350  vitali  25593  mbfi1fseqlem4  25698  aannenlem1  26308  perfect  27211  2lgsoddprmlem3  27394  2sq2  27413  ltsval2  27637  bday0b  27822  negs11  28058  elnns2  28350  n0cutlt  28368  umgrislfupgrlem  29208  usgrausgrb  29255  upgriswlk  29727  uhgrwkspth  29841  usgr2wlkspth  29845  usgr2trlspth  29847  usgr2pthspth  29848  extwwlkfab  30440  grporcan  30607  grpolcan  30619  ip2eqi  30945  hial2eq  31195  eigorthi  31926  stge1i  32327  stle0i  32328  mdbr3  32386  mdbr4  32387  atsseq  32436  mdsymlem7  32498  reuxfrdf  32578  disjunsn  32682  fpwrelmapffslem  32823  xmulcand  32998  prsdm  34077  prsrn  34078  lfuhgr  35319  lfuhgr2  35320  mthmpps  35783  untangtr  35915  filnetlem4  36582  ordtopconn  36640  ordtopt0  36643  bj-dfbi6  36859  bj-spvew  36949  bj-19.9htbi  37019  bj-axseprep  37400  bj-elid6  37503  icorempo  37684  inunissunidif  37708  fvineqsneu  37744  wl-lem-moexsb  37910  seqpo  38085  qmapeldisjsbi  39199  lshpcmp  39451  lsatcmp  39466  lsatcmp2  39467  ltrneq2  40611  ltrneq  40612  tendospcanN  41486  dochlkr  41848  lcfl7N  41964  hgmap11  42365  ccatcan2d  42707  remulcan2d  42712  itrere  42767  log11d  42795  resubcan2  42837  readdcan2  42862  sn-addcand  42869  sn-addcan2d  42871  remulcand  42888  sn-itrere  42950  sn-retire  42951  cnreeu  42952  fphpd  43265  pellexlem3  43280  qirropth  43357  expdioph  43472  rpnnen3  43481  iotasbc  44867  f1ocof1ob2  47545  2reu3  47573  rlimdmafv  47640  afv2orxorb  47691  rlimdmafv2  47721  funop1  47746  2ffzoeq  47791  prprelprb  47992  poprelb  47999  evenprm2  48205  perfectALTV  48214  nnsum3primesle9  48285  upgrwlkupwlkb  48632  islinindfis  48940  lincresunit3lem3  48965  blen1b  49079  line2ylem  49242  line2y  49246  intubeu  49474  unilbeu  49475  thincn0eu  49921