Theorem impbid1 228

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 215	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  impbid2  229  iba  531  pm5.61  1001  pm5.71  1028  cad0  1625  cad0OLD  1626  19.33b  1893  19.40b  1896  19.9t  2204  axc16gb  2261  equs5  2459  2eu1  2651  2eu1v  2652  2eu3  2654  ceqsalgALT  3431  eqvincg  3545  reuxfrd  3650  2reu1  3796  disjeq0  4356  undif4  4367  ssprsseq  4724  sneqbg  4740  preq1b  4743  opthpr  4748  preq12nebg  4759  opthprneg  4761  elpwuni  4999  disjxiun  5036  eusv2i  5272  reusv2lem3  5278  reusv3  5283  soltmin  5981  ssxpb  6017  xp11  6018  xpcan  6019  xpcan2  6020  ordssun  6290  suc11  6294  unizlim  6308  imadif  6442  2elresin  6476  mpteqb  6815  f1fveq  7052  f1elima  7053  f1imass  7054  fliftf  7102  sorpssuni  7498  sorpssint  7499  iunpw  7534  ssonprc  7549  onint0  7553  oa00  8265  omcan  8275  omopth2  8290  oecan  8295  nnarcl  8322  iserd  8395  mapfset  8509  map0g  8543  fundmen  8686  fopwdom  8731  onfin  8846  fineqvlem  8868  f1finf1o  8880  isfiniteg  8909  inficl  9019  tc00  9342  cardnueq0  9545  cardsdomel  9555  wdomfil  9640  wdomnumr  9643  alephsucdom  9658  cardalephex  9669  dfac12lem2  9723  cfeq0  9835  fin23lem24  9901  fin1a2lem9  9987  carden  10130  axrepnd  10173  axacndlem4  10189  gchpwdom  10249  gchina  10278  r1tskina  10361  addcanpi  10478  mulcanpi  10479  elnpi  10567  addcan  10981  addcan2  10982  neg11  11094  negreb  11108  add20  11309  mulcand  11430  cru  11787  nn0lt10b  12204  uz11  12428  eqreznegel  12495  lbzbi  12497  rpnnen1lem6  12543  xrmaxlt  12736  xrltmin  12737  xrmaxle  12738  xrlemin  12739  xneg11  12770  xnn0xadd0  12802  xsubge0  12816  xrub  12867  elioc2  12963  elico2  12964  elicc2  12965  fzopth  13114  2ffzeq  13198  flidz  13350  addmodlteq  13484  expeq0  13630  sq01  13757  fz1eqb  13886  hashen1  13902  hash1snb  13951  hashle2pr  14008  wrdnval  14065  eqwrd  14077  ccatalpha  14115  wrdl1s1  14136  ccats1alpha  14141  ccatopth  14246  ccatopth2  14247  wrdlen2  14474  cj11  14690  sqrt0  14770  abs00  14818  recan  14865  cnsqrt00  14921  rlimdm  15077  rpnnen2lem12  15749  0dvds  15801  dvds1  15843  alzdvds  15844  nn0enne  15901  nn0oddm1d2  15909  nnoddm1d2  15910  gcdeq0  16039  algcvgblem  16097  2mulprm  16213  prmexpb  16240  prmreclem3  16434  4sqlem11  16471  moni  17195  grprcan  18355  grplcan  18379  grpinv11  18386  galcan  18652  sylow2a  18962  subgdisjb  19037  drngmuleq0  19744  lspsncmp  20107  fidomndrng  20299  xrsdsreclb  20364  znidomb  20480  lmisfree  20758  coe1tm  21148  tgdom  21829  en1top  21835  cmpfi  22259  txcmpb  22495  hmeocnvb  22625  flimcls  22836  hauspwpwf1  22838  flftg  22847  ghmcnp  22966  metrest  23376  icoopnst  23790  iocopnst  23791  ishl2  24221  vitali  24464  mbfi1fseqlem4  24570  aannenlem1  25175  perfect  26066  2lgsoddprmlem3  26249  2sq2  26268  umgrislfupgrlem  27167  usgrausgrb  27214  upgriswlk  27682  uhgrwkspth  27796  usgr2wlkspth  27800  usgr2trlspth  27802  usgr2pthspth  27803  extwwlkfab  28389  grporcan  28553  grpolcan  28565  ip2eqi  28891  hial2eq  29141  eigorthi  29872  stge1i  30273  stle0i  30274  mdbr3  30332  mdbr4  30333  atsseq  30382  mdsymlem7  30444  reuxfrdf  30512  disjunsn  30606  fpwrelmapffslem  30741  xmulcand  30869  prsdm  31532  prsrn  31533  lfuhgr  32746  lfuhgr2  32747  mthmpps  33211  untangtr  33322  funeldmb  33407  sltval2  33545  bday0b  33710  filnetlem4  34256  ordtopconn  34314  ordtopt0  34317  bj-dfbi6  34442  bj-19.9htbi  34571  bj-elid6  35025  icorempo  35208  inunissunidif  35232  fvineqsneu  35268  wl-lem-moexsb  35409  seqpo  35591  lshpcmp  36688  lsatcmp  36703  lsatcmp2  36704  ltrneq2  37848  ltrneq  37849  tendospcanN  38723  dochlkr  39085  lcfl7N  39201  hgmap11  39602  ccatcan2d  39873  remulcan2d  39941  resubcan2  40020  readdcan2  40044  sn-addcand  40050  sn-addcan2d  40052  remulcand  40069  itrere  40085  retire  40086  cnreeu  40087  fphpd  40282  pellexlem3  40297  qirropth  40374  expdioph  40489  rpnnen3  40498  iotasbc  41651  f1ocof1ob2  44189  2reu3  44217  rlimdmafv  44284  afv2orxorb  44335  rlimdmafv2  44365  funop1  44390  fzoopth  44435  2ffzoeq  44436  prprelprb  44585  poprelb  44592  evenprm2  44782  perfectALTV  44791  nnsum3primesle9  44862  upgrwlkupwlkb  44919  0ringdif  45044  islinindfis  45406  lincresunit3lem3  45431  blen1b  45550  line2ylem  45713  line2y  45717  intubeu  45886  unilbeu  45887  thincn0eu  45929