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  536  pm5.61  1016  pm5.71  1045  cad0  1648  19.33b  1915  19.40b  1918  19.9t  2240  axc16gb  2298  equs5  2492  2eu1  2678  2eu1v  2679  2eu3  2681  ceqsalgALT  3491  eqvincg  3607  reuxfrd  3711  2reu1  3851  disjeq0  4416  undif4  4427  iftrueb  4500  ssprsseq  4791  sneqbg  4808  preq1b  4811  opthpr  4816  preq12nebg  4828  opthprneg  4830  dfiun2g  4994  elpwuni  5071  disjxiun  5106  eusv2i  5365  reusv2lem3  5371  reusv3  5376  soltmin  6136  ssxpb  6172  xp11  6173  xpcan  6174  xpcan2  6175  ordssun  6465  suc11  6470  unizlim  6485  imadif  6620  2elresin  6656  mpteqb  7009  f1fveq  7260  f1elima  7261  f1imass  7262  fliftf  7313  funeldmb  7357  sorpssuni  7729  sorpssint  7730  iunpw  7766  ssonprc  7782  onint0  7786  oa00  8540  omcan  8550  omopth2  8565  oecan  8571  nnarcl  8598  iserd  8717  mapfset  8843  map0g  8878  fundmen  9024  fopwdom  9069  onfin  9195  0sdom1dom  9202  fineqvlem  9222  f1finf1o  9229  isfiniteg  9256  inficl  9381  tc00  9711  cardnueq0  9946  cardsdomel  9956  wdomfil  10041  wdomnumr  10044  alephsucdom  10059  cardalephex  10070  dfac12lem2  10124  cfeq0  10235  fin23lem24  10301  fin1a2lem9  10387  carden  10530  axrepnd  10574  axacndlem4  10590  gchpwdom  10650  gchina  10679  r1tskina  10762  addcanpi  10879  mulcanpi  10880  elnpi  10968  addcan  11389  addcan2  11390  neg11  11504  negreb  11518  add20  11721  mulcand  11842  cru  12205  nn0lt10b  12653  uz11  12882  eqreznegel  12953  lbzbi  12955  rpnnen1lem6  13001  xrmaxlt  13202  xrltmin  13203  xrmaxle  13204  xrlemin  13205  xneg11  13236  xnn0xadd0  13268  xsubge0  13282  xrub  13333  elioc2  13431  elico2  13432  elicc2  13433  fzopth  13585  2ffzeq  13673  fzoopth  13787  flidz  13839  addmodlteq  13978  expeq0  14124  sq01  14257  fz1eqb  14386  hashen1  14402  hash1snb  14452  hashle2pr  14510  wrdnval  14578  eqwrd  14590  ccatalpha  14627  wrdl1s1  14648  ccats1alpha  14653  ccatopth  14749  ccatopth2  14750  wrdlen2  14977  cj11  15209  sqrt0  15288  abs00  15336  recan  15384  cnsqrt00  15440  rlimdm  15598  rpnnen2lem12  16276  0dvds  16329  dvds1  16372  alzdvds  16373  nn0enne  16430  nn0oddm1d2  16438  nnoddm1d2  16439  gcdeq0  16570  algcvgblem  16630  2mulprm  16746  prmexpb  16773  prmreclem3  16973  4sqlem11  17010  moni  17788  chnfibg  18687  grprcan  19035  grplcan  19062  grpinv11  19069  galcan  19369  sylow2a  19684  subgdisjb  19758  0ringdif  20625  domnlcanb  20818  domnrcanb  20820  drngmuleq0  20866  fidomndrng  20877  lspsncmp  21240  xrsdsreclb  21564  znidomb  21711  lmisfree  21992  coe1tm  22434  tgdom  23135  en1top  23141  cmpfi  23565  txcmpb  23801  hmeocnvb  23931  flimcls  24142  hauspwpwf1  24144  flftg  24153  ghmcnp  24272  metrest  24681  icoopnst  25098  iocopnst  25099  ishl2  25529  vitali  25772  mbfi1fseqlem4  25877  aannenlem1  26491  perfect  27395  2lgsoddprmlem3  27578  2sq2  27597  ltsval2  27820  bday0b  28006  negs11  28242  elnns2  28534  n0cutlt  28552  umgrislfupgrlem  29472  usgrausgrb  29519  upgriswlk  29990  uhgrwkspth  30104  usgr2wlkspth  30108  usgr2trlspth  30110  usgr2pthspth  30111  extwwlkfab  30703  grporcan  30870  grpolcan  30882  ip2eqi  31208  hial2eq  31458  eigorthi  32189  stge1i  32590  stle0i  32591  mdbr3  32649  mdbr4  32650  atsseq  32699  mdsymlem7  32761  reuxfrdf  32837  disjunsn  32939  fpwrelmapffslem  33077  xmulcand  33240  prsdm  34304  prsrn  34305  lfuhgr  35610  lfuhgr2  35611  mthmpps  36074  untangtr  36206  filnetlem4  36912  ordtopconn  36970  ordtopt0  36973  bj-dfbi6  37188  bj-spvew  37278  bj-19.9htbi  37348  bj-axseprep  37731  bj-elid6  37834  icorempo  38017  inunissunidif  38041  fvineqsneu  38077  wl-lem-moexsb  38243  seqpo  38418  qmapeldisjsbi  39530  lshpcmp  39782  lsatcmp  39797  lsatcmp2  39798  ltrneq2  40942  ltrneq  40943  tendospcanN  41817  dochlkr  42179  lcfl7N  42295  hgmap11  42696  ccatcan2d  43039  remulcan2d  43044  itrere  43099  log11d  43127  resubcan2  43169  readdcan2  43194  sn-addcand  43201  sn-addcan2d  43203  remulcand  43220  sn-itrere  43282  sn-retire  43283  cnreeu  43284  fphpd  43563  pellexlem3  43578  qirropth  43655  expdioph  43770  rpnnen3  43779  iotasbc  45149  f1ocof1ob2  47839  2reu3  47867  rlimdmafv  47934  afv2orxorb  47985  rlimdmafv2  48015  funop1  48040  2ffzoeq  48085  prprelprb  48286  poprelb  48293  evenprm2  48499  perfectALTV  48508  nnsum3primesle9  48579  upgrwlkupwlkb  48926  islinindfis  49249  lincresunit3lem3  49274  blen1b  49388  line2ylem  49551  line2y  49555  intubeu  49782  unilbeu  49783  thincn0eu  50229