Theorem imbi1d 341

Description: Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)

Hypothesis

Ref	Expression
imbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
imbi1d	⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))

Proof of Theorem imbi1d

Step	Hyp	Ref	Expression
1		imbid.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimprd 248	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	imim1d 82	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) → (𝜒 → 𝜃)))
4	1	biimpd 229	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
5	4	imim1d 82	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))
6	3, 5	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:  imbi12d  344  imbi1  347  imim21b  394  pm5.33  835  con3ALT  1084  norasslem3  1536  sbjust  2064  sbequ  2084  sb6  2086  19.21t  2207  sb4b  2473  drsb1  2493  cbvralsvw  3281  sbralie  3317  raleqf  3320  ralcom2  3342  rmoeq1  3378  rspceaimv  3585  ralxpxfr2d  3603  alexeqg  3608  elab6g  3626  mo2icl  3676  sbc19.21g  3816  csbiebg  3885  ralss  4012  ralssOLD  4014  r19.37zv  4455  reuprg0  4656  unissb  4893  intmin4  4930  dftr2c  5205  ssexg  5265  pocl  5539  vtoclr  5686  frsn  5711  cotrg  6064  dffun2  6496  fun11  6560  funimass4  6891  dff13  7195  f1mpt  7202  isopolem  7286  fnssintima  7303  oprabidw  7384  oprabid  7385  caovcan  7557  imaeqalov  7592  caoftrn  7658  ordunisuc2  7784  tfisi  7799  tfinds  7800  tfindsg  7801  tfindsg2  7802  dfom2  7808  findsg  7837  frxp  8066  xpord2indlem  8087  xpord3inddlem  8094  poseq  8098  frrlem12  8237  dfsmo2  8277  qliftfun  8736  ecoptocl  8741  ecopovtrn  8754  dom2lem  8924  findcard  9087  findcard2  9088  ssfi  9097  findcard3  9187  findcard3OLD  9188  fiint  9235  fiintOLD  9236  supmo  9361  eqsup  9365  suplub  9369  supisoex  9384  infmo  9406  wemaplem1  9457  wemaplem2  9458  wemapsolem  9461  oemapvali  9599  cantnf  9608  wemapwe  9612  ttrclss  9635  karden  9810  aceq1  10030  zorn2lem1  10409  axrepndlem2  10506  axregndlem2  10516  gruurn  10711  indpi  10820  nqereu  10842  prcdnq  10906  supexpr  10967  ltsosr  11007  supsrlem  11024  supsr  11025  axpre-lttrn  11079  axpre-sup  11082  prodgt0  11990  infm3  12103  prime  12576  raluz  12816  zsupss  12857  uzsupss  12860  xrsupsslem  13228  xrinfmsslem  13229  fz1sbc  13522  ssnn0fi  13911  fi1uzind  14433  brfi1indALT  14436  wrdind  14647  wrd2ind  14648  relexprelg  14964  rtrclreclem3  14986  relexpindlem  14989  relexpind  14990  rtrclind  14991  rexanre  15273  rexico  15280  reusq0  15391  limsupgle  15403  ello12  15442  ello12r  15443  ello1d  15449  elo12  15453  elo12r  15454  lo1resb  15490  o1resb  15492  rlimcn3  15516  addcn2  15520  mulcn2  15522  lo1le  15578  rpnnen2lem12  16153  sqrt2irr  16177  dfgcd2  16476  exprmfct  16634  isprm5  16637  isprm7  16638  prmdvdsexpr  16647  prmpwdvds  16835  vdwmc2  16910  ramtlecl  16931  ramub  16944  rami  16946  ramcl  16960  firest  17355  mreexexd  17573  acsfn  17584  prslem  18222  ispos  18239  posi  18242  isposd  18247  pospropd  18250  lubeldm  18276  lubval  18279  glbeldm  18289  glbval  18292  joinval2lem  18303  meetval2lem  18317  resspos  18354  odlem1  19433  mndodcongi  19441  gexlem1  19477  sylow1lem3  19498  efgredlemb  19644  efgred  19646  frgpnabllem1  19771  isrrg  20602  isdomn4  20620  domnlcanb  20624  domnrcanb  20626  acsfn1p  20703  xrsdsreclb  21339  islindf4  21764  mplsubglem  21925  mpllsslem  21926  ltbval  21967  opsrval  21970  psdmul  22070  mdetunilem1  22516  mdetunilem3  22518  mdetunilem4  22519  mdetunilem9  22524  chpscmat  22746  istopg  22799  isclo2  22992  neiptoptop  23035  neiptopnei  23036  lmbr  23162  ist0  23224  ist1-2  23251  t1sep2  23273  cmpfi  23312  2ndcdisj  23360  1stccn  23367  iskgen3  23453  ptpjopn  23516  hausdiag  23549  xkopt  23559  ist0-4  23633  isr0  23641  r0sep  23652  fbfinnfr  23745  fmfnfmlem2  23859  fmfnfmlem4  23861  fmfnfm  23862  cnflf  23906  cnfcf  23946  tmdgsum2  24000  tsmsf1o  24049  tsmsxplem1  24057  ustssel  24110  ustincl  24112  ustdiag  24113  ustinvel  24114  ustexhalf  24115  ust0  24124  ustuqtop4  24149  utopsnneiplem  24152  isucn2  24183  iducn  24187  metcnp  24446  txmetcnp  24452  metucn  24476  ngptgp  24541  nlmvscnlem1  24591  xrge0tsms  24740  xmetdcn2  24743  addcnlem  24770  ipcnlem1  25162  caucfil  25200  metcld  25223  metcld2  25224  ellimc2  25795  dvne0  25933  mdegleb  25986  mdegle0  25999  ply1divex  26059  fta1g  26092  dgrco  26198  plydivex  26222  fta1  26233  vieta1  26237  cxpcn3lem  26674  rlimcnp  26892  mpodvdsmulf1o  27121  dvdsmulf1o  27123  ppiublem1  27130  dchrinv  27189  lgseisenlem2  27304  2sqlem6  27351  2sqlem8  27354  2sqlem10  27356  nocvxminlem  27707  addsprop  27907  sleadd1  27920  negsprop  27965  mulsprop  28057  bdayon  28197  onsfi  28271  expsne0  28347  istrkgc  28418  istrkgb  28419  axtgcgrid  28427  axtg5seg  28429  axtgpasch  28431  axtgeucl  28436  tgcgr4  28495  axlowdimlem15  28920  usgr2wlkneq  29720  usgr2pthlem  29727  friendshipgt3  30361  isnvlem  30573  vacn  30657  smcnlem  30660  norm3lemt  31115  isch2  31186  chlimi  31197  omlsii  31366  eigorth  31801  stcltr1i  32237  elat2  32303  funcnv5mpt  32630  xrge0infss  32722  sgn3da  32798  sgnnbi  32802  sgnpbi  32803  wrdt2ind  32914  xrge0tsmsd  33034  elrgspnlem4  33204  domnlcanOLD  33238  islinds5  33323  islbs5  33336  prmidlval  33393  rprmdvdspow  33489  1arithufdlem3  33502  evl1deg1  33530  evl1deg2  33531  evl1deg3  33532  ply1dg1rt  33534  ist0cld  33819  qqhucn  33978  esum2d  34079  eulerpartlemgvv  34363  tgoldbachgt  34650  axtgupdim2ALTV  34655  bnj1145  34979  bnj1171  34986  bnj1172  34987  tz9.1regs  35086  isacycgr1  35138  acycgrcycl  35139  erdszelem8  35190  satfrnmapom  35362  mclsval  35555  mclsax  35561  mclsppslem  35575  climuzcnv  35663  elintfv  35757  ifscgr  36037  idinside  36077  brsegle  36101  ixpeq12dv  36209  trer  36309  filnetlem4  36374  bj-ssblem1  36647  bj-ssblem2  36648  bj-ax12  36650  bj-19.21t0  36823  mobidvALT  36850  currysetlem  36938  currysetlem1  36940  wl-ax12v2cl  37499  wl-sbrimt  37540  fin2so  37606  ptrecube  37619  poimirlem26  37645  poimirlem27  37646  heicant  37654  mbfresfi  37665  itg2addnc  37673  filbcmb  37739  sdclem2  37741  fdc  37744  fdc1  37745  rngoidmlem  37935  divrngidl  38027  pridlval  38032  smprngopr  38051  inecmo  38342  elcnvrefrels3  38531  disjlem18  38797  ax12inda  38946  ax12v2-o  38947  isat3  39305  iscvlat2N  39322  psubspset  39743  ldilfset  40107  ldilset  40108  dilfsetN  40151  dilsetN  40152  cdlemefrs29bpre0  40395  cdlemefrs29clN  40398  cdlemefrs32fva  40399  cdlemn11pre  41209  dihord2pre  41224  lpolsetN  41481  isprimroot  42086  primrootsunit1  42090  primrootscoprbij  42095  aks6d1c1  42109  hashscontpow  42115  sticksstones11  42149  sticksstones12a  42150  aks6d1c6lem3  42165  fimgmcyc  42527  fsuppind  42583  aomclem8  43054  hbtlem5  43121  unielss  43211  ifpbi1  43470  ifpbi12  43481  ifpbi13  43482  ntrneik2  44085  ntrneikb  44087  gneispacess2  44139  2sbc6g  44408  sbiota1  44427  relpeq2  44939  nregmodel  45011  uzwo4  45051  iineq12dv  45104  fsumiunss  45576  limsupre  45642  limsupref  45686  limsupbnd1f  45687  limsupmnf  45722  limsupre2  45726  limsupmnfuzlem  45727  limsupre2mpt  45731  limsupre3  45734  limsupre3mpt  45735  ioodvbdlimc1lem2  45933  ioodvbdlimc2lem  45935  dvmptfprodlem  45945  wallispilem3  46068  fourierdlem48  46155  sge0f1o  46383  sge0iunmptlemre  46416  sge0iunmpt  46419  vonioo  46683  vonicc  46686  fcoresf1  47073  2reu8i  47117  2reuimp0  47118  2reuimp  47119  sprsymrelfolem2  47497  paireqne  47515  nfermltlrev  47748  bgoldbachlt  47817  tgoldbachlt  47820  gpgedgiov  48069  gpgedg2ov  48070  gpgedg2iv  48071  pgnbgreunbgrlem1  48117  pgnbgreunbgrlem3  48122  pgnbgreunbgrlem4  48123  pgnbgreunbgrlem6  48128  pgnbgreunbgr  48129  ply1mulgsumlem1  48391  ply1mulgsumlem2  48392  elbigo2  48557  elbigo2r  48558  logic1  48795  postcposALT  49573  postc  49574  setrecseq  49690  setrec1lem1  49692  aacllem  49806