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  1618  19.33b  1885  19.40b  1888  19.9t  2204  axc16gb  2262  equs5  2465  2eu1  2651  2eu1v  2652  2eu3  2654  ceqsalgALT  3518  eqvincg  3648  reuxfrd  3754  2reu1  3897  disjeq0  4456  undif4  4467  iftrueb  4538  ssprsseq  4825  sneqbg  4843  preq1b  4846  opthpr  4851  preq12nebg  4863  opthprneg  4865  dfiun2g  5030  elpwuni  5105  disjxiun  5140  eusv2i  5394  reusv2lem3  5400  reusv3  5405  soltmin  6156  ssxpb  6194  xp11  6195  xpcan  6196  xpcan2  6197  ordssun  6486  suc11  6491  unizlim  6507  imadif  6650  2elresin  6689  mpteqb  7035  f1fveq  7282  f1elima  7283  f1imass  7284  fliftf  7335  funeldmb  7379  sorpssuni  7752  sorpssint  7753  iunpw  7791  ssonprc  7807  onint0  7811  oa00  8597  omcan  8607  omopth2  8622  oecan  8627  nnarcl  8654  iserd  8771  mapfset  8890  map0g  8924  fundmen  9071  fopwdom  9120  onfin  9267  0sdom1dom  9274  fineqvlem  9298  f1finf1o  9305  f1finf1oOLD  9306  isfiniteg  9337  inficl  9465  tc00  9788  cardnueq0  10004  cardsdomel  10014  wdomfil  10101  wdomnumr  10104  alephsucdom  10119  cardalephex  10130  dfac12lem2  10185  cfeq0  10296  fin23lem24  10362  fin1a2lem9  10448  carden  10591  axrepnd  10634  axacndlem4  10650  gchpwdom  10710  gchina  10739  r1tskina  10822  addcanpi  10939  mulcanpi  10940  elnpi  11028  addcan  11445  addcan2  11446  neg11  11560  negreb  11574  add20  11775  mulcand  11896  cru  12258  nn0lt10b  12680  uz11  12903  eqreznegel  12976  lbzbi  12978  rpnnen1lem6  13024  xrmaxlt  13223  xrltmin  13224  xrmaxle  13225  xrlemin  13226  xneg11  13257  xnn0xadd0  13289  xsubge0  13303  xrub  13354  elioc2  13450  elico2  13451  elicc2  13452  fzopth  13601  2ffzeq  13689  fzoopth  13801  flidz  13850  addmodlteq  13987  expeq0  14133  sq01  14264  fz1eqb  14393  hashen1  14409  hash1snb  14458  hashle2pr  14516  wrdnval  14583  eqwrd  14595  ccatalpha  14631  wrdl1s1  14652  ccats1alpha  14657  ccatopth  14754  ccatopth2  14755  wrdlen2  14983  cj11  15201  sqrt0  15280  abs00  15328  recan  15375  cnsqrt00  15431  rlimdm  15587  rpnnen2lem12  16261  0dvds  16314  dvds1  16356  alzdvds  16357  nn0enne  16414  nn0oddm1d2  16422  nnoddm1d2  16423  gcdeq0  16554  algcvgblem  16614  2mulprm  16730  prmexpb  16756  prmreclem3  16956  4sqlem11  16993  moni  17780  grprcan  18991  grplcan  19018  grpinv11  19025  grpinv11OLD  19026  galcan  19322  sylow2a  19637  subgdisjb  19711  0ringdif  20527  domnlcanb  20720  domnrcanb  20722  drngmuleq0  20763  fidomndrng  20774  lspsncmp  21118  xrsdsreclb  21431  znidomb  21580  lmisfree  21862  coe1tm  22276  tgdom  22985  en1top  22991  cmpfi  23416  txcmpb  23652  hmeocnvb  23782  flimcls  23993  hauspwpwf1  23995  flftg  24004  ghmcnp  24123  metrest  24537  icoopnst  24969  iocopnst  24970  ishl2  25404  vitali  25648  mbfi1fseqlem4  25753  aannenlem1  26370  perfect  27275  2lgsoddprmlem3  27458  2sq2  27477  sltval2  27701  bday0b  27875  negs11  28081  elnns2  28344  umgrislfupgrlem  29139  usgrausgrb  29186  upgriswlk  29659  uhgrwkspth  29775  usgr2wlkspth  29779  usgr2trlspth  29781  usgr2pthspth  29782  extwwlkfab  30371  grporcan  30537  grpolcan  30549  ip2eqi  30875  hial2eq  31125  eigorthi  31856  stge1i  32257  stle0i  32258  mdbr3  32316  mdbr4  32317  atsseq  32366  mdsymlem7  32428  reuxfrdf  32510  disjunsn  32607  fpwrelmapffslem  32743  xmulcand  32903  prsdm  33913  prsrn  33914  lfuhgr  35123  lfuhgr2  35124  mthmpps  35587  untangtr  35714  filnetlem4  36382  ordtopconn  36440  ordtopt0  36443  bj-dfbi6  36576  bj-19.9htbi  36704  bj-elid6  37171  icorempo  37352  inunissunidif  37376  fvineqsneu  37412  wl-lem-moexsb  37569  seqpo  37754  lshpcmp  38989  lsatcmp  39004  lsatcmp2  39005  ltrneq2  40150  ltrneq  40151  tendospcanN  41025  dochlkr  41387  lcfl7N  41503  hgmap11  41904  ccatcan2d  42292  remulcan2d  42298  itrere  42353  log11d  42382  resubcan2  42418  readdcan2  42442  sn-addcand  42449  sn-addcan2d  42451  remulcand  42468  sn-itrere  42498  sn-retire  42499  cnreeu  42500  fphpd  42827  pellexlem3  42842  qirropth  42919  expdioph  43035  rpnnen3  43044  iotasbc  44438  f1ocof1ob2  47094  2reu3  47122  rlimdmafv  47189  afv2orxorb  47240  rlimdmafv2  47270  funop1  47295  2ffzoeq  47339  prprelprb  47504  poprelb  47511  evenprm2  47701  perfectALTV  47710  nnsum3primesle9  47781  upgrwlkupwlkb  48057  islinindfis  48366  lincresunit3lem3  48391  blen1b  48509  line2ylem  48672  line2y  48676  intubeu  48873  unilbeu  48874  thincn0eu  49080