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  1537  sbjust  2066  sbequ  2088  sb6  2090  19.21t  2213  sb4b  2479  drsb1  2499  cbvralsvw  3287  sbralie  3322  raleqf  3325  ralcom2  3347  rmoeq1  3381  rspceaimv  3582  ralxpxfr2d  3600  alexeqg  3605  elab6g  3623  mo2icl  3672  sbc19.21g  3812  csbiebg  3881  ralss  4008  ralssOLD  4010  r19.37zv  4460  reuprg0  4659  unissb  4896  intmin4  4932  dftr2c  5208  ssexg  5268  pocl  5540  vtoclr  5687  frsn  5712  cotrg  6068  dffun2  6502  fun11  6566  funimass4  6898  dff13  7200  f1mpt  7207  isopolem  7291  fnssintima  7308  oprabidw  7389  oprabid  7390  caovcan  7562  imaeqalov  7597  caoftrn  7663  ordunisuc2  7786  tfisi  7801  tfinds  7802  tfindsg  7803  tfindsg2  7804  dfom2  7810  findsg  7839  frxp  8068  xpord2indlem  8089  xpord3inddlem  8096  poseq  8100  frrlem12  8239  dfsmo2  8279  qliftfun  8739  ecoptocl  8744  ecopovtrn  8757  dom2lem  8929  findcard  9088  findcard2  9089  ssfi  9097  findcard3  9183  fiint  9227  supmo  9355  eqsup  9359  suplub  9363  supisoex  9378  infmo  9400  wemaplem1  9451  wemaplem2  9452  wemapsolem  9455  oemapvali  9593  cantnf  9602  wemapwe  9606  ttrclss  9629  karden  9807  aceq1  10027  zorn2lem1  10406  axrepndlem2  10504  axregndlem2  10514  gruurn  10709  indpi  10818  nqereu  10840  prcdnq  10904  supexpr  10965  ltsosr  11005  supsrlem  11022  supsr  11023  axpre-lttrn  11077  axpre-sup  11080  prodgt0  11988  infm3  12101  prime  12573  raluz  12809  zsupss  12850  uzsupss  12853  xrsupsslem  13222  xrinfmsslem  13223  fz1sbc  13516  ssnn0fi  13908  fi1uzind  14430  brfi1indALT  14433  wrdind  14645  wrd2ind  14646  relexprelg  14961  rtrclreclem3  14983  relexpindlem  14986  relexpind  14987  rtrclind  14988  rexanre  15270  rexico  15277  reusq0  15388  limsupgle  15400  ello12  15439  ello12r  15440  ello1d  15446  elo12  15450  elo12r  15451  lo1resb  15487  o1resb  15489  rlimcn3  15513  addcn2  15517  mulcn2  15519  lo1le  15575  rpnnen2lem12  16150  sqrt2irr  16174  dfgcd2  16473  exprmfct  16631  isprm5  16634  isprm7  16635  prmdvdsexpr  16644  prmpwdvds  16832  vdwmc2  16907  ramtlecl  16928  ramub  16941  rami  16943  ramcl  16957  firest  17352  mreexexd  17571  acsfn  17582  prslem  18220  ispos  18237  posi  18240  isposd  18245  pospropd  18248  lubeldm  18274  lubval  18277  glbeldm  18287  glbval  18290  joinval2lem  18301  meetval2lem  18315  resspos  18352  odlem1  19464  mndodcongi  19472  gexlem1  19508  sylow1lem3  19529  efgredlemb  19675  efgred  19677  frgpnabllem1  19802  isrrg  20631  isdomn4  20649  domnlcanb  20653  domnrcanb  20655  acsfn1p  20732  xrsdsreclb  21368  islindf4  21793  mplsubglem  21954  mpllsslem  21955  ltbval  21998  opsrval  22001  psdmul  22109  mdetunilem1  22556  mdetunilem3  22558  mdetunilem4  22559  mdetunilem9  22564  chpscmat  22786  istopg  22839  isclo2  23032  neiptoptop  23075  neiptopnei  23076  lmbr  23202  ist0  23264  ist1-2  23291  t1sep2  23313  cmpfi  23352  2ndcdisj  23400  1stccn  23407  iskgen3  23493  ptpjopn  23556  hausdiag  23589  xkopt  23599  ist0-4  23673  isr0  23681  r0sep  23692  fbfinnfr  23785  fmfnfmlem2  23899  fmfnfmlem4  23901  fmfnfm  23902  cnflf  23946  cnfcf  23986  tmdgsum2  24040  tsmsf1o  24089  tsmsxplem1  24097  ustssel  24150  ustincl  24152  ustdiag  24153  ustinvel  24154  ustexhalf  24155  ust0  24164  ustuqtop4  24188  utopsnneiplem  24191  isucn2  24222  iducn  24226  metcnp  24485  txmetcnp  24491  metucn  24515  ngptgp  24580  nlmvscnlem1  24630  xrge0tsms  24779  xmetdcn2  24782  addcnlem  24809  ipcnlem1  25201  caucfil  25239  metcld  25262  metcld2  25263  ellimc2  25834  dvne0  25972  mdegleb  26025  mdegle0  26038  ply1divex  26098  fta1g  26131  dgrco  26237  plydivex  26261  fta1  26272  vieta1  26276  cxpcn3lem  26713  rlimcnp  26931  mpodvdsmulf1o  27160  dvdsmulf1o  27162  ppiublem1  27169  dchrinv  27228  lgseisenlem2  27343  2sqlem6  27390  2sqlem8  27393  2sqlem10  27395  nocvxminlem  27750  addsprop  27972  leadds1  27985  negsprop  28031  mulsprop  28126  bdayons  28272  onsfi  28352  expsne0  28432  istrkgc  28526  istrkgb  28527  axtgcgrid  28535  axtg5seg  28537  axtgpasch  28539  axtgeucl  28544  tgcgr4  28603  axlowdimlem15  29029  usgr2wlkneq  29829  usgr2pthlem  29836  friendshipgt3  30473  isnvlem  30685  vacn  30769  smcnlem  30772  norm3lemt  31227  isch2  31298  chlimi  31309  omlsii  31478  eigorth  31913  stcltr1i  32349  elat2  32415  funcnv5mpt  32746  xrge0infss  32840  sgn3da  32915  sgnnbi  32919  sgnpbi  32920  wrdt2ind  33035  xrge0tsmsd  33155  elrgspnlem4  33327  domnlcanOLD  33362  islinds5  33448  islbs5  33461  prmidlval  33518  rprmdvdspow  33614  1arithufdlem3  33627  evl1deg1  33657  evl1deg2  33658  evl1deg3  33659  ply1dg1rt  33661  ist0cld  33990  qqhucn  34149  esum2d  34250  eulerpartlemgvv  34533  tgoldbachgt  34820  axtgupdim2ALTV  34825  bnj1145  35149  bnj1171  35156  bnj1172  35157  tz9.1regs  35290  isacycgr1  35340  acycgrcycl  35341  erdszelem8  35392  satfrnmapom  35564  mclsval  35757  mclsax  35763  mclsppslem  35777  climuzcnv  35865  elintfv  35959  ifscgr  36238  idinside  36278  brsegle  36302  ixpeq12dv  36410  trer  36510  filnetlem4  36575  mh-setindnd  36667  bj-ssblem1  36855  bj-ssblem2  36856  bj-ax12  36858  bj-19.21t0  37031  mobidvALT  37058  currysetlem  37146  currysetlem1  37148  wl-ax12v2cl  37711  wl-sbrimt  37752  fin2so  37808  ptrecube  37821  poimirlem26  37847  poimirlem27  37848  heicant  37856  mbfresfi  37867  itg2addnc  37875  filbcmb  37941  sdclem2  37943  fdc  37946  fdc1  37947  rngoidmlem  38137  divrngidl  38229  pridlval  38234  smprngopr  38253  inecmo  38548  elcnvrefrels3  38788  disjlem18  39059  ax12inda  39208  ax12v2-o  39209  isat3  39567  iscvlat2N  39584  psubspset  40004  ldilfset  40368  ldilset  40369  dilfsetN  40412  dilsetN  40413  cdlemefrs29bpre0  40656  cdlemefrs29clN  40659  cdlemefrs32fva  40660  cdlemn11pre  41470  dihord2pre  41485  lpolsetN  41742  isprimroot  42347  primrootsunit1  42351  primrootscoprbij  42356  aks6d1c1  42370  hashscontpow  42376  sticksstones11  42410  sticksstones12a  42411  aks6d1c6lem3  42426  fimgmcyc  42789  fsuppind  42833  aomclem8  43303  hbtlem5  43370  unielss  43460  ifpbi1  43718  ifpbi12  43729  ifpbi13  43730  ntrneik2  44333  ntrneikb  44335  gneispacess2  44387  2sbc6g  44656  sbiota1  44675  relpeq2  45186  nregmodel  45258  uzwo4  45298  iineq12dv  45350  fsumiunss  45821  limsupre  45885  limsupref  45929  limsupbnd1f  45930  limsupmnf  45965  limsupre2  45969  limsupmnfuzlem  45970  limsupre2mpt  45974  limsupre3  45977  limsupre3mpt  45978  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  dvmptfprodlem  46188  wallispilem3  46311  fourierdlem48  46398  sge0f1o  46626  sge0iunmptlemre  46659  sge0iunmpt  46662  vonioo  46926  vonicc  46929  fcoresf1  47315  2reu8i  47359  2reuimp0  47360  2reuimp  47361  sprsymrelfolem2  47739  paireqne  47757  nfermltlrev  47990  bgoldbachlt  48059  tgoldbachlt  48062  gpgedgiov  48311  gpgedg2ov  48312  gpgedg2iv  48313  pgnbgreunbgrlem1  48359  pgnbgreunbgrlem3  48364  pgnbgreunbgrlem4  48365  pgnbgreunbgrlem6  48370  pgnbgreunbgr  48371  ply1mulgsumlem1  48632  ply1mulgsumlem2  48633  elbigo2  48798  elbigo2r  48799  logic1  49036  postcposALT  49813  postc  49814  setrecseq  49930  setrec1lem1  49932  aacllem  50046