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  1618  19.33b  1885  19.40b  1888  19.9t  2205  axc16gb  2263  equs5  2458  2eu1  2644  2eu1v  2645  2eu3  2647  ceqsalgALT  3481  eqvincg  3611  reuxfrd  3716  2reu1  3857  disjeq0  4415  undif4  4426  iftrueb  4497  ssprsseq  4785  sneqbg  4803  preq1b  4806  opthpr  4811  preq12nebg  4823  opthprneg  4825  dfiun2g  4990  elpwuni  5064  disjxiun  5099  eusv2i  5344  reusv2lem3  5350  reusv3  5355  soltmin  6097  ssxpb  6135  xp11  6136  xpcan  6137  xpcan2  6138  ordssun  6424  suc11  6429  unizlim  6445  imadif  6584  2elresin  6621  mpteqb  6969  f1fveq  7219  f1elima  7220  f1imass  7221  fliftf  7272  funeldmb  7316  sorpssuni  7688  sorpssint  7689  iunpw  7727  ssonprc  7743  onint0  7747  oa00  8500  omcan  8510  omopth2  8525  oecan  8530  nnarcl  8557  iserd  8674  mapfset  8800  map0g  8834  fundmen  8979  fopwdom  9026  onfin  9156  0sdom1dom  9162  fineqvlem  9185  f1finf1o  9192  f1finf1oOLD  9193  isfiniteg  9224  inficl  9352  tc00  9677  cardnueq0  9893  cardsdomel  9903  wdomfil  9990  wdomnumr  9993  alephsucdom  10008  cardalephex  10019  dfac12lem2  10074  cfeq0  10185  fin23lem24  10251  fin1a2lem9  10337  carden  10480  axrepnd  10523  axacndlem4  10539  gchpwdom  10599  gchina  10628  r1tskina  10711  addcanpi  10828  mulcanpi  10829  elnpi  10917  addcan  11334  addcan2  11335  neg11  11449  negreb  11463  add20  11666  mulcand  11787  cru  12154  nn0lt10b  12572  uz11  12794  eqreznegel  12869  lbzbi  12871  rpnnen1lem6  12917  xrmaxlt  13117  xrltmin  13118  xrmaxle  13119  xrlemin  13120  xneg11  13151  xnn0xadd0  13183  xsubge0  13197  xrub  13248  elioc2  13346  elico2  13347  elicc2  13348  fzopth  13498  2ffzeq  13586  fzoopth  13699  flidz  13748  addmodlteq  13887  expeq0  14033  sq01  14166  fz1eqb  14295  hashen1  14311  hash1snb  14360  hashle2pr  14418  wrdnval  14486  eqwrd  14498  ccatalpha  14534  wrdl1s1  14555  ccats1alpha  14560  ccatopth  14657  ccatopth2  14658  wrdlen2  14886  cj11  15104  sqrt0  15183  abs00  15231  recan  15279  cnsqrt00  15335  rlimdm  15493  rpnnen2lem12  16169  0dvds  16222  dvds1  16265  alzdvds  16266  nn0enne  16323  nn0oddm1d2  16331  nnoddm1d2  16332  gcdeq0  16463  algcvgblem  16523  2mulprm  16639  prmexpb  16665  prmreclem3  16865  4sqlem11  16902  moni  17678  grprcan  18887  grplcan  18914  grpinv11  18921  grpinv11OLD  18922  galcan  19218  sylow2a  19533  subgdisjb  19607  0ringdif  20447  domnlcanb  20640  domnrcanb  20642  drngmuleq0  20683  fidomndrng  20693  lspsncmp  21058  xrsdsreclb  21355  znidomb  21503  lmisfree  21784  coe1tm  22192  tgdom  22898  en1top  22904  cmpfi  23328  txcmpb  23564  hmeocnvb  23694  flimcls  23905  hauspwpwf1  23907  flftg  23916  ghmcnp  24035  metrest  24445  icoopnst  24869  iocopnst  24870  ishl2  25303  vitali  25547  mbfi1fseqlem4  25652  aannenlem1  26269  perfect  27175  2lgsoddprmlem3  27358  2sq2  27377  sltval2  27601  bday0b  27779  negs11  27995  elnns2  28273  n0cutlt  28289  umgrislfupgrlem  29102  usgrausgrb  29149  upgriswlk  29621  uhgrwkspth  29735  usgr2wlkspth  29739  usgr2trlspth  29741  usgr2pthspth  29742  extwwlkfab  30331  grporcan  30497  grpolcan  30509  ip2eqi  30835  hial2eq  31085  eigorthi  31816  stge1i  32217  stle0i  32218  mdbr3  32276  mdbr4  32277  atsseq  32326  mdsymlem7  32388  reuxfrdf  32470  disjunsn  32573  fpwrelmapffslem  32705  xmulcand  32891  prsdm  33897  prsrn  33898  lfuhgr  35098  lfuhgr2  35099  mthmpps  35562  untangtr  35694  filnetlem4  36362  ordtopconn  36420  ordtopt0  36423  bj-dfbi6  36556  bj-19.9htbi  36684  bj-elid6  37151  icorempo  37332  inunissunidif  37356  fvineqsneu  37392  wl-lem-moexsb  37549  seqpo  37734  lshpcmp  38974  lsatcmp  38989  lsatcmp2  38990  ltrneq2  40135  ltrneq  40136  tendospcanN  41010  dochlkr  41372  lcfl7N  41488  hgmap11  41889  ccatcan2d  42232  remulcan2d  42238  itrere  42299  log11d  42327  resubcan2  42369  readdcan2  42394  sn-addcand  42401  sn-addcan2d  42403  remulcand  42420  sn-itrere  42469  sn-retire  42470  cnreeu  42471  fphpd  42797  pellexlem3  42812  qirropth  42889  expdioph  43005  rpnnen3  43014  iotasbc  44401  f1ocof1ob2  47076  2reu3  47104  rlimdmafv  47171  afv2orxorb  47222  rlimdmafv2  47252  funop1  47277  2ffzoeq  47321  prprelprb  47511  poprelb  47518  evenprm2  47708  perfectALTV  47717  nnsum3primesle9  47788  upgrwlkupwlkb  48122  islinindfis  48431  lincresunit3lem3  48456  blen1b  48570  line2ylem  48733  line2y  48737  intubeu  48965  unilbeu  48966  thincn0eu  49413