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  3484  eqvincg  3614  reuxfrd  3719  2reu1  3860  disjeq0  4419  undif4  4430  iftrueb  4501  ssprsseq  4789  sneqbg  4807  preq1b  4810  opthpr  4815  preq12nebg  4827  opthprneg  4829  dfiun2g  4994  elpwuni  5069  disjxiun  5104  eusv2i  5349  reusv2lem3  5355  reusv3  5360  soltmin  6109  ssxpb  6147  xp11  6148  xpcan  6149  xpcan2  6150  ordssun  6436  suc11  6441  unizlim  6457  imadif  6600  2elresin  6639  mpteqb  6987  f1fveq  7237  f1elima  7238  f1imass  7239  fliftf  7290  funeldmb  7334  sorpssuni  7708  sorpssint  7709  iunpw  7747  ssonprc  7763  onint0  7767  oa00  8523  omcan  8533  omopth2  8548  oecan  8553  nnarcl  8580  iserd  8697  mapfset  8823  map0g  8857  fundmen  9002  fopwdom  9049  onfin  9179  0sdom1dom  9185  fineqvlem  9209  f1finf1o  9216  f1finf1oOLD  9217  isfiniteg  9248  inficl  9376  tc00  9701  cardnueq0  9917  cardsdomel  9927  wdomfil  10014  wdomnumr  10017  alephsucdom  10032  cardalephex  10043  dfac12lem2  10098  cfeq0  10209  fin23lem24  10275  fin1a2lem9  10361  carden  10504  axrepnd  10547  axacndlem4  10563  gchpwdom  10623  gchina  10652  r1tskina  10735  addcanpi  10852  mulcanpi  10853  elnpi  10941  addcan  11358  addcan2  11359  neg11  11473  negreb  11487  add20  11690  mulcand  11811  cru  12178  nn0lt10b  12596  uz11  12818  eqreznegel  12893  lbzbi  12895  rpnnen1lem6  12941  xrmaxlt  13141  xrltmin  13142  xrmaxle  13143  xrlemin  13144  xneg11  13175  xnn0xadd0  13207  xsubge0  13221  xrub  13272  elioc2  13370  elico2  13371  elicc2  13372  fzopth  13522  2ffzeq  13610  fzoopth  13723  flidz  13772  addmodlteq  13911  expeq0  14057  sq01  14190  fz1eqb  14319  hashen1  14335  hash1snb  14384  hashle2pr  14442  wrdnval  14510  eqwrd  14522  ccatalpha  14558  wrdl1s1  14579  ccats1alpha  14584  ccatopth  14681  ccatopth2  14682  wrdlen2  14910  cj11  15128  sqrt0  15207  abs00  15255  recan  15303  cnsqrt00  15359  rlimdm  15517  rpnnen2lem12  16193  0dvds  16246  dvds1  16289  alzdvds  16290  nn0enne  16347  nn0oddm1d2  16355  nnoddm1d2  16356  gcdeq0  16487  algcvgblem  16547  2mulprm  16663  prmexpb  16689  prmreclem3  16889  4sqlem11  16926  moni  17698  grprcan  18905  grplcan  18932  grpinv11  18939  grpinv11OLD  18940  galcan  19236  sylow2a  19549  subgdisjb  19623  0ringdif  20436  domnlcanb  20629  domnrcanb  20631  drngmuleq0  20672  fidomndrng  20682  lspsncmp  21026  xrsdsreclb  21330  znidomb  21471  lmisfree  21751  coe1tm  22159  tgdom  22865  en1top  22871  cmpfi  23295  txcmpb  23531  hmeocnvb  23661  flimcls  23872  hauspwpwf1  23874  flftg  23883  ghmcnp  24002  metrest  24412  icoopnst  24836  iocopnst  24837  ishl2  25270  vitali  25514  mbfi1fseqlem4  25619  aannenlem1  26236  perfect  27142  2lgsoddprmlem3  27325  2sq2  27344  sltval2  27568  bday0b  27742  negs11  27955  elnns2  28233  n0cutlt  28249  umgrislfupgrlem  29049  usgrausgrb  29096  upgriswlk  29569  uhgrwkspth  29685  usgr2wlkspth  29689  usgr2trlspth  29691  usgr2pthspth  29692  extwwlkfab  30281  grporcan  30447  grpolcan  30459  ip2eqi  30785  hial2eq  31035  eigorthi  31766  stge1i  32167  stle0i  32168  mdbr3  32226  mdbr4  32227  atsseq  32276  mdsymlem7  32338  reuxfrdf  32420  disjunsn  32523  fpwrelmapffslem  32655  xmulcand  32841  prsdm  33904  prsrn  33905  lfuhgr  35105  lfuhgr2  35106  mthmpps  35569  untangtr  35701  filnetlem4  36369  ordtopconn  36427  ordtopt0  36430  bj-dfbi6  36563  bj-19.9htbi  36691  bj-elid6  37158  icorempo  37339  inunissunidif  37363  fvineqsneu  37399  wl-lem-moexsb  37556  seqpo  37741  lshpcmp  38981  lsatcmp  38996  lsatcmp2  38997  ltrneq2  40142  ltrneq  40143  tendospcanN  41017  dochlkr  41379  lcfl7N  41495  hgmap11  41896  ccatcan2d  42239  remulcan2d  42245  itrere  42306  log11d  42334  resubcan2  42376  readdcan2  42401  sn-addcand  42408  sn-addcan2d  42410  remulcand  42427  sn-itrere  42476  sn-retire  42477  cnreeu  42478  fphpd  42804  pellexlem3  42819  qirropth  42896  expdioph  43012  rpnnen3  43021  iotasbc  44408  f1ocof1ob2  47083  2reu3  47111  rlimdmafv  47178  afv2orxorb  47229  rlimdmafv2  47259  funop1  47284  2ffzoeq  47328  prprelprb  47518  poprelb  47525  evenprm2  47715  perfectALTV  47724  nnsum3primesle9  47795  upgrwlkupwlkb  48129  islinindfis  48438  lincresunit3lem3  48463  blen1b  48577  line2ylem  48740  line2y  48744  intubeu  48972  unilbeu  48973  thincn0eu  49420