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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  impbid2  229  iba  537  pm5.61  1016  pm5.71  1045  cad0  1651  19.33b  1918  19.40b  1921  19.9t  2243  axc16gb  2300  equs5  2494  2eu1  2680  2eu1v  2681  2eu3  2683  ceqsalgALT  3493  eqvincg  3609  reuxfrd  3713  2reu1  3852  disjeq0  4416  undif4  4427  iftrueb  4502  ssprsseq  4793  sneqbg  4810  preq1b  4813  opthpr  4818  preq12nebg  4830  opthprneg  4832  dfiun2g  4996  elpwuni  5073  disjxiun  5108  eusv2i  5367  reusv2lem3  5373  reusv3  5378  soltmin  6138  ssxpb  6174  xp11  6175  xpcan  6176  xpcan2  6177  ordssun  6469  suc11  6474  unizlim  6489  imadif  6624  2elresin  6660  mpteqb  7013  f1fveq  7265  f1elima  7266  f1imass  7267  fliftf  7322  funeldmb  7368  sorpssuni  7739  sorpssint  7740  iunpw  7776  ssonprc  7792  onint0  7796  oa00  8550  omcan  8560  omopth2  8575  oecan  8581  nnarcl  8608  iserd  8727  mapfset  8853  map0g  8888  fundmen  9035  fopwdom  9080  onfin  9206  0sdom1dom  9213  fineqvlem  9233  f1finf1o  9240  isfiniteg  9267  inficl  9392  tc00  9722  cardnueq0  9966  cardsdomel  9976  wdomfil  10061  wdomnumr  10064  alephsucdom  10079  cardalephex  10090  dfac12lem2  10144  cfeq0  10255  fin23lem24  10321  fin1a2lem9  10407  carden  10552  axrepnd  10596  axacndlem4  10612  gchpwdom  10672  gchina  10701  r1tskina  10784  addcanpi  10901  mulcanpi  10902  elnpi  10990  addcan  11411  addcan2  11412  neg11  11526  negreb  11540  add20  11743  mulcand  11864  cru  12227  nn0lt10b  12676  uz11  12905  eqreznegel  12976  lbzbi  12978  rpnnen1lem6  13024  xrmaxlt  13225  xrltmin  13226  xrmaxle  13227  xrlemin  13228  xneg11  13259  xnn0xadd0  13291  xsubge0  13305  xrub  13356  elioc2  13454  elico2  13455  elicc2  13456  fzopth  13608  2ffzeq  13696  fzoopth  13810  flidz  13863  addmodlteq  14002  expeq0  14148  sq01  14281  fz1eqb  14410  hashen1  14426  hash1snb  14476  hashle2pr  14534  wrdnval  14602  eqwrd  14614  ccatalpha  14652  wrdl1s1  14674  ccats1alpha  14679  ccatopth  14777  ccatopth2  14778  wrdlen2  15007  cj11  15239  sqrt0  15318  abs00  15366  recan  15414  cnsqrt00  15470  rlimdm  15628  rpnnen2lem12  16305  0dvds  16358  dvds1  16401  alzdvds  16402  nn0enne  16459  nn0oddm1d2  16467  nnoddm1d2  16468  gcdeq0  16599  algcvgblem  16659  2mulprm  16775  prmexpb  16802  prmreclem3  17002  4sqlem11  17039  moni  17817  chnfibg  18716  grprcan  19086  grplcan  19113  grpinv11  19120  galcan  19420  sylow2a  19735  subgdisjb  19809  0ringdif  20677  domnlcanb  20870  domnrcanb  20872  drngmuleq0  20918  fidomndrng  20929  lspsncmp  21292  xrsdsreclb  21616  znidomb  21763  lmisfree  22044  coe1tm  22486  tgdom  23187  en1top  23193  cmpfi  23617  txcmpb  23854  hmeocnvb  23984  flimcls  24195  hauspwpwf1  24197  flftg  24206  ghmcnp  24325  metrest  24734  icoopnst  25151  iocopnst  25152  ishl2  25582  vitali  25825  mbfi1fseqlem4  25930  aannenlem1  26544  perfect  27448  2lgsoddprmlem3  27631  2sq2  27650  ltsval2  27873  bday0b  28059  negs11  28295  elnns2  28587  n0cutlt  28605  umgrislfupgrlem  29529  lfuhgr  29555  lfuhgr2  29556  usgrausgrb  29579  upgriswlk  30050  uhgrwkspth  30170  usgr2wlkspth  30174  usgr2trlspth  30176  usgr2pthspth  30177  extwwlkfab  30776  grporcan  30943  grpolcan  30955  ip2eqi  31281  hial2eq  31531  eigorthi  32262  stge1i  32663  stle0i  32664  mdbr3  32722  mdbr4  32723  atsseq  32772  mdsymlem7  32834  reuxfrdf  32910  disjunsn  33012  fpwrelmapffslem  33149  xmulcand  33312  prsdm  34370  prsrn  34371  mthmpps  36113  untangtr  36245  filnetlem4  36951  ordtopconn  37009  ordtopt0  37012  bj-dfbi6  37227  bj-spvew  37317  bj-19.9htbi  37387  bj-axseprep  37770  bj-elid6  37873  icorempo  38056  inunissunidif  38080  fvineqsneu  38116  wl-lem-moexsb  38282  seqpo  38458  qmapeldisjsbi  39570  lshpcmp  39822  lsatcmp  39837  lsatcmp2  39838  ltrneq2  40982  ltrneq  40983  tendospcanN  41857  dochlkr  42219  lcfl7N  42335  hgmap11  42736  ccatcan2d  43079  remulcan2d  43084  itrere  43139  log11d  43167  resubcan2  43209  readdcan2  43234  sn-addcand  43241  sn-addcan2d  43243  remulcand  43260  sn-itrere  43322  sn-retire  43323  cnreeu  43324  fphpd  43603  pellexlem3  43618  qirropth  43695  expdioph  43810  rpnnen3  43819  iotasbc  45189  f1ocof1ob2  47879  2reu3  47907  rlimdmafv  47974  afv2orxorb  48025  rlimdmafv2  48055  funop1  48080  2ffzoeq  48125  prprelprb  48326  poprelb  48333  evenprm2  48539  perfectALTV  48548  nnsum3primesle9  48619  upgrwlkupwlkb  48966  islinindfis  49288  lincresunit3lem3  49313  blen1b  49427  line2ylem  49590  line2y  49594  intubeu  49821  unilbeu  49822  thincn0eu  50268