Theorem impbid1 227

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  impbid2  228  iba  535  pm5.61  1014  pm5.71  1041  cad0  1638  19.33b  1905  19.40b  1908  19.9t  2239  axc16gb  2297  equs5  2491  2eu1  2677  2eu1v  2678  2eu3  2680  ceqsalgALT  3490  eqvincg  3607  reuxfrd  3711  2reu1  3850  disjeq0  4410  undif4  4421  iftrueb  4493  ssprsseq  4783  sneqbg  4801  preq1b  4804  opthpr  4809  preq12nebg  4821  opthprneg  4823  dfiun2g  4987  elpwuni  5062  disjxiun  5097  eusv2i  5351  reusv2lem3  5357  reusv3  5362  soltmin  6123  ssxpb  6160  xp11  6161  xpcan  6162  xpcan2  6163  ordssun  6450  suc11  6455  unizlim  6470  imadif  6605  2elresin  6642  mpteqb  6995  f1fveq  7246  f1elima  7247  f1imass  7248  fliftf  7299  funeldmb  7343  sorpssuni  7715  sorpssint  7716  iunpw  7754  ssonprc  7770  onint0  7774  oa00  8528  omcan  8538  omopth2  8553  oecan  8559  nnarcl  8586  iserd  8705  mapfset  8831  map0g  8866  fundmen  9012  fopwdom  9057  onfin  9183  0sdom1dom  9190  fineqvlem  9210  f1finf1o  9217  isfiniteg  9244  inficl  9371  tc00  9701  cardnueq0  9922  cardsdomel  9932  wdomfil  10017  wdomnumr  10020  alephsucdom  10035  cardalephex  10046  dfac12lem2  10101  cfeq0  10213  fin23lem24  10279  fin1a2lem9  10365  carden  10508  axrepnd  10552  axacndlem4  10568  gchpwdom  10628  gchina  10657  r1tskina  10740  addcanpi  10857  mulcanpi  10858  elnpi  10946  addcan  11367  addcan2  11368  neg11  11482  negreb  11496  add20  11699  mulcand  11820  cru  12187  nn0lt10b  12635  uz11  12864  eqreznegel  12935  lbzbi  12937  rpnnen1lem6  12983  xrmaxlt  13184  xrltmin  13185  xrmaxle  13186  xrlemin  13187  xneg11  13218  xnn0xadd0  13250  xsubge0  13264  xrub  13315  elioc2  13413  elico2  13414  elicc2  13415  fzopth  13566  2ffzeq  13654  fzoopth  13768  flidz  13820  addmodlteq  13959  expeq0  14105  sq01  14238  fz1eqb  14367  hashen1  14383  hash1snb  14432  hashle2pr  14490  wrdnval  14558  eqwrd  14570  ccatalpha  14607  wrdl1s1  14628  ccats1alpha  14633  ccatopth  14729  ccatopth2  14730  wrdlen2  14957  cj11  15189  sqrt0  15268  abs00  15316  recan  15364  cnsqrt00  15420  rlimdm  15578  rpnnen2lem12  16257  0dvds  16310  dvds1  16353  alzdvds  16354  nn0enne  16411  nn0oddm1d2  16419  nnoddm1d2  16420  gcdeq0  16551  algcvgblem  16611  2mulprm  16727  prmexpb  16754  prmreclem3  16954  4sqlem11  16991  moni  17769  chnfibg  18668  grprcan  19015  grplcan  19042  grpinv11  19049  grpinv11OLD  19050  galcan  19344  sylow2a  19659  subgdisjb  19733  0ringdif  20577  domnlcanb  20770  domnrcanb  20772  drngmuleq0  20813  fidomndrng  20823  lspsncmp  21186  xrsdsreclb  21466  znidomb  21613  lmisfree  21894  coe1tm  22336  tgdom  23038  en1top  23044  cmpfi  23468  txcmpb  23704  hmeocnvb  23834  flimcls  24045  hauspwpwf1  24047  flftg  24056  ghmcnp  24175  metrest  24584  icoopnst  25001  iocopnst  25002  ishl2  25432  vitali  25675  mbfi1fseqlem4  25780  aannenlem1  26392  perfect  27295  2lgsoddprmlem3  27478  2sq2  27497  ltsval2  27720  bday0b  27906  negs11  28142  elnns2  28434  n0cutlt  28452  umgrislfupgrlem  29323  usgrausgrb  29370  upgriswlk  29841  uhgrwkspth  29955  usgr2wlkspth  29959  usgr2trlspth  29961  usgr2pthspth  29962  extwwlkfab  30554  grporcan  30721  grpolcan  30733  ip2eqi  31059  hial2eq  31309  eigorthi  32040  stge1i  32441  stle0i  32442  mdbr3  32500  mdbr4  32501  atsseq  32550  mdsymlem7  32612  reuxfrdf  32690  disjunsn  32794  fpwrelmapffslem  32934  xmulcand  33098  prsdm  34211  prsrn  34212  lfuhgr  35468  lfuhgr2  35469  mthmpps  35932  untangtr  36064  filnetlem4  36741  ordtopconn  36799  ordtopt0  36802  bj-dfbi6  37018  bj-spvew  37108  bj-19.9htbi  37178  bj-axseprep  37559  bj-elid6  37662  icorempo  37845  inunissunidif  37869  fvineqsneu  37905  wl-lem-moexsb  38071  seqpo  38246  qmapeldisjsbi  39360  lshpcmp  39612  lsatcmp  39627  lsatcmp2  39628  ltrneq2  40772  ltrneq  40773  tendospcanN  41647  dochlkr  42009  lcfl7N  42125  hgmap11  42526  ccatcan2d  42867  remulcan2d  42872  itrere  42927  log11d  42955  resubcan2  42997  readdcan2  43022  sn-addcand  43029  sn-addcan2d  43031  remulcand  43048  sn-itrere  43110  sn-retire  43111  cnreeu  43112  fphpd  43393  pellexlem3  43408  qirropth  43485  expdioph  43600  rpnnen3  43609  iotasbc  44995  f1ocof1ob2  47676  2reu3  47704  rlimdmafv  47771  afv2orxorb  47822  rlimdmafv2  47852  funop1  47877  2ffzoeq  47922  prprelprb  48123  poprelb  48130  evenprm2  48336  perfectALTV  48345  nnsum3primesle9  48416  upgrwlkupwlkb  48763  islinindfis  49071  lincresunit3lem3  49096  blen1b  49210  line2ylem  49373  line2y  49377  intubeu  49605  unilbeu  49606  thincn0eu  50052