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  836  con3ALT  1085  norasslem3  1538  sbjust  2067  sbequ  2089  sb6  2091  19.21t  2214  sb4b  2480  drsb1  2500  cbvralsvw  3289  sbralie  3324  raleqf  3327  ralcom2  3349  rmoeq1  3383  rspceaimv  3584  ralxpxfr2d  3602  alexeqg  3607  elab6g  3625  mo2icl  3674  sbc19.21g  3814  csbiebg  3883  ralss  4010  ralssOLD  4012  r19.37zv  4462  reuprg0  4661  unissb  4898  intmin4  4934  dftr2c  5210  ssexg  5270  pocl  5548  vtoclr  5695  frsn  5720  cotrg  6076  dffun2  6510  fun11  6574  funimass4  6906  dff13  7210  f1mpt  7217  isopolem  7301  fnssintima  7318  oprabidw  7399  oprabid  7400  caovcan  7572  imaeqalov  7607  caoftrn  7673  ordunisuc2  7796  tfisi  7811  tfinds  7812  tfindsg  7813  tfindsg2  7814  dfom2  7820  findsg  7849  frxp  8078  xpord2indlem  8099  xpord3inddlem  8106  poseq  8110  frrlem12  8249  dfsmo2  8289  qliftfun  8751  ecoptocl  8756  ecopovtrn  8769  dom2lem  8941  findcard  9100  findcard2  9101  ssfi  9109  findcard3  9195  fiint  9239  supmo  9367  eqsup  9371  suplub  9375  supisoex  9390  infmo  9412  wemaplem1  9463  wemaplem2  9464  wemapsolem  9467  oemapvali  9605  cantnf  9614  wemapwe  9618  ttrclss  9641  karden  9819  aceq1  10039  zorn2lem1  10418  axrepndlem2  10516  axregndlem2  10526  gruurn  10721  indpi  10830  nqereu  10852  prcdnq  10916  supexpr  10977  ltsosr  11017  supsrlem  11034  supsr  11035  axpre-lttrn  11089  axpre-sup  11092  prodgt0  12000  infm3  12113  prime  12585  raluz  12821  zsupss  12862  uzsupss  12865  xrsupsslem  13234  xrinfmsslem  13235  fz1sbc  13528  ssnn0fi  13920  fi1uzind  14442  brfi1indALT  14445  wrdind  14657  wrd2ind  14658  relexprelg  14973  rtrclreclem3  14995  relexpindlem  14998  relexpind  14999  rtrclind  15000  rexanre  15282  rexico  15289  reusq0  15400  limsupgle  15412  ello12  15451  ello12r  15452  ello1d  15458  elo12  15462  elo12r  15463  lo1resb  15499  o1resb  15501  rlimcn3  15525  addcn2  15529  mulcn2  15531  lo1le  15587  rpnnen2lem12  16162  sqrt2irr  16186  dfgcd2  16485  exprmfct  16643  isprm5  16646  isprm7  16647  prmdvdsexpr  16656  prmpwdvds  16844  vdwmc2  16919  ramtlecl  16940  ramub  16953  rami  16955  ramcl  16969  firest  17364  mreexexd  17583  acsfn  17594  prslem  18232  ispos  18249  posi  18252  isposd  18257  pospropd  18260  lubeldm  18286  lubval  18289  glbeldm  18299  glbval  18302  joinval2lem  18313  meetval2lem  18327  resspos  18364  odlem1  19476  mndodcongi  19484  gexlem1  19520  sylow1lem3  19541  efgredlemb  19687  efgred  19689  frgpnabllem1  19814  isrrg  20643  isdomn4  20661  domnlcanb  20665  domnrcanb  20667  acsfn1p  20744  xrsdsreclb  21380  islindf4  21805  mplsubglem  21966  mpllsslem  21967  ltbval  22010  opsrval  22013  psdmul  22121  mdetunilem1  22568  mdetunilem3  22570  mdetunilem4  22571  mdetunilem9  22576  chpscmat  22798  istopg  22851  isclo2  23044  neiptoptop  23087  neiptopnei  23088  lmbr  23214  ist0  23276  ist1-2  23303  t1sep2  23325  cmpfi  23364  2ndcdisj  23412  1stccn  23419  iskgen3  23505  ptpjopn  23568  hausdiag  23601  xkopt  23611  ist0-4  23685  isr0  23693  r0sep  23704  fbfinnfr  23797  fmfnfmlem2  23911  fmfnfmlem4  23913  fmfnfm  23914  cnflf  23958  cnfcf  23998  tmdgsum2  24052  tsmsf1o  24101  tsmsxplem1  24109  ustssel  24162  ustincl  24164  ustdiag  24165  ustinvel  24166  ustexhalf  24167  ust0  24176  ustuqtop4  24200  utopsnneiplem  24203  isucn2  24234  iducn  24238  metcnp  24497  txmetcnp  24503  metucn  24527  ngptgp  24592  nlmvscnlem1  24642  xrge0tsms  24791  xmetdcn2  24794  addcnlem  24821  ipcnlem1  25213  caucfil  25251  metcld  25274  metcld2  25275  ellimc2  25846  dvne0  25984  mdegleb  26037  mdegle0  26050  ply1divex  26110  fta1g  26143  dgrco  26249  plydivex  26273  fta1  26284  vieta1  26288  cxpcn3lem  26725  rlimcnp  26943  mpodvdsmulf1o  27172  dvdsmulf1o  27174  ppiublem1  27181  dchrinv  27240  lgseisenlem2  27355  2sqlem6  27402  2sqlem8  27405  2sqlem10  27407  nocvxminlem  27762  addsprop  27984  leadds1  27997  negsprop  28043  mulsprop  28138  bdayons  28284  onsfi  28364  expsne0  28444  istrkgc  28538  istrkgb  28539  axtgcgrid  28547  axtg5seg  28549  axtgpasch  28551  axtgeucl  28556  tgcgr4  28615  axlowdimlem15  29041  usgr2wlkneq  29841  usgr2pthlem  29848  friendshipgt3  30485  isnvlem  30698  vacn  30782  smcnlem  30785  norm3lemt  31240  isch2  31311  chlimi  31322  omlsii  31491  eigorth  31926  stcltr1i  32362  elat2  32428  funcnv5mpt  32757  xrge0infss  32851  sgn3da  32926  sgnnbi  32930  sgnpbi  32931  wrdt2ind  33046  xrge0tsmsd  33167  elrgspnlem4  33339  domnlcanOLD  33374  islinds5  33460  islbs5  33473  prmidlval  33530  rprmdvdspow  33626  1arithufdlem3  33639  evl1deg1  33669  evl1deg2  33670  evl1deg3  33671  ply1dg1rt  33673  ist0cld  34011  qqhucn  34170  esum2d  34271  eulerpartlemgvv  34554  tgoldbachgt  34841  axtgupdim2ALTV  34846  bnj1145  35169  bnj1171  35176  bnj1172  35177  tz9.1regs  35312  isacycgr1  35362  acycgrcycl  35363  erdszelem8  35414  satfrnmapom  35586  mclsval  35779  mclsax  35785  mclsppslem  35799  climuzcnv  35887  elintfv  35981  ifscgr  36260  idinside  36300  brsegle  36324  ixpeq12dv  36432  trer  36532  filnetlem4  36597  mh-setindnd  36689  bj-ssblem1  36899  bj-ssblem2  36900  bj-ax12  36902  bj-19.21t0  37078  mobidvALT  37105  currysetlem  37193  currysetlem1  37195  wl-ax12v2cl  37761  wl-sbrimt  37802  fin2so  37858  ptrecube  37871  poimirlem26  37897  poimirlem27  37898  heicant  37906  mbfresfi  37917  itg2addnc  37925  filbcmb  37991  sdclem2  37993  fdc  37996  fdc1  37997  rngoidmlem  38187  divrngidl  38279  pridlval  38284  smprngopr  38303  inecmo  38606  elcnvrefrels3  38866  eldisjdmqsim2  39067  qmapeldisjsim  39111  rnqmapeleldisjsim  39113  disjlem18  39154  ax12inda  39324  ax12v2-o  39325  isat3  39683  iscvlat2N  39700  psubspset  40120  ldilfset  40484  ldilset  40485  dilfsetN  40528  dilsetN  40529  cdlemefrs29bpre0  40772  cdlemefrs29clN  40775  cdlemefrs32fva  40776  cdlemn11pre  41586  dihord2pre  41601  lpolsetN  41858  isprimroot  42463  primrootsunit1  42467  primrootscoprbij  42472  aks6d1c1  42486  hashscontpow  42492  sticksstones11  42526  sticksstones12a  42527  aks6d1c6lem3  42542  fimgmcyc  42904  fsuppind  42948  aomclem8  43418  hbtlem5  43485  unielss  43575  ifpbi1  43833  ifpbi12  43844  ifpbi13  43845  ntrneik2  44448  ntrneikb  44450  gneispacess2  44502  2sbc6g  44771  sbiota1  44790  relpeq2  45301  nregmodel  45373  uzwo4  45413  iineq12dv  45465  fsumiunss  45935  limsupre  45999  limsupref  46043  limsupbnd1f  46044  limsupmnf  46079  limsupre2  46083  limsupmnfuzlem  46084  limsupre2mpt  46088  limsupre3  46091  limsupre3mpt  46092  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  dvmptfprodlem  46302  wallispilem3  46425  fourierdlem48  46512  sge0f1o  46740  sge0iunmptlemre  46773  sge0iunmpt  46776  vonioo  47040  vonicc  47043  fcoresf1  47429  2reu8i  47473  2reuimp0  47474  2reuimp  47475  sprsymrelfolem2  47853  paireqne  47871  nfermltlrev  48104  bgoldbachlt  48173  tgoldbachlt  48176  gpgedgiov  48425  gpgedg2ov  48426  gpgedg2iv  48427  pgnbgreunbgrlem1  48473  pgnbgreunbgrlem3  48478  pgnbgreunbgrlem4  48479  pgnbgreunbgrlem6  48484  pgnbgreunbgr  48485  ply1mulgsumlem1  48746  ply1mulgsumlem2  48747  elbigo2  48912  elbigo2r  48913  logic1  49150  postcposALT  49927  postc  49928  setrecseq  50044  setrec1lem1  50046  aacllem  50160