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  2479  drsb1  2499  cbvralsvw  3288  sbralie  3315  raleqf  3318  ralcom2  3339  rmoeq1  3373  rspceaimv  3570  ralxpxfr2d  3588  alexeqg  3593  elab6g  3611  mo2icl  3660  sbc19.21g  3800  csbiebg  3869  ralss  3996  ralssOLD  3998  r19.37zv  4447  reuprg0  4646  unissb  4883  intmin4  4919  dftr2c  5195  ssexg  5264  pocl  5547  vtoclr  5694  frsn  5719  cotrg  6074  dffun2  6508  fun11  6572  funimass4  6904  dff13  7209  f1mpt  7216  isopolem  7300  fnssintima  7317  oprabidw  7398  oprabid  7399  caovcan  7571  imaeqalov  7606  caoftrn  7672  ordunisuc2  7795  tfisi  7810  tfinds  7811  tfindsg  7812  tfindsg2  7813  dfom2  7819  findsg  7848  frxp  8076  xpord2indlem  8097  xpord3inddlem  8104  poseq  8108  frrlem12  8247  dfsmo2  8287  qliftfun  8749  ecoptocl  8754  ecopovtrn  8767  dom2lem  8939  findcard  9098  findcard2  9099  ssfi  9107  findcard3  9193  fiint  9237  supmo  9365  eqsup  9369  suplub  9373  supisoex  9388  infmo  9410  wemaplem1  9461  wemaplem2  9462  wemapsolem  9465  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  12002  infm3  12115  prime  12610  raluz  12846  zsupss  12887  uzsupss  12890  xrsupsslem  13259  xrinfmsslem  13260  fz1sbc  13554  ssnn0fi  13947  fi1uzind  14469  brfi1indALT  14472  wrdind  14684  wrd2ind  14685  relexprelg  15000  rtrclreclem3  15022  relexpindlem  15025  relexpind  15026  rtrclind  15027  rexanre  15309  rexico  15316  reusq0  15427  limsupgle  15439  ello12  15478  ello12r  15479  ello1d  15485  elo12  15489  elo12r  15490  lo1resb  15526  o1resb  15528  rlimcn3  15552  addcn2  15556  mulcn2  15558  lo1le  15614  rpnnen2lem12  16192  sqrt2irr  16216  dfgcd2  16515  exprmfct  16674  isprm5  16677  isprm7  16678  prmdvdsexpr  16687  prmpwdvds  16875  vdwmc2  16950  ramtlecl  16971  ramub  16984  rami  16986  ramcl  17000  firest  17395  mreexexd  17614  acsfn  17625  prslem  18263  ispos  18280  posi  18283  isposd  18288  pospropd  18291  lubeldm  18317  lubval  18320  glbeldm  18330  glbval  18333  joinval2lem  18344  meetval2lem  18358  resspos  18395  odlem1  19510  mndodcongi  19518  gexlem1  19554  sylow1lem3  19575  efgredlemb  19721  efgred  19723  frgpnabllem1  19848  isrrg  20675  isdomn4  20693  domnlcanb  20697  domnrcanb  20699  acsfn1p  20776  xrsdsreclb  21394  islindf4  21818  mplsubglem  21977  mpllsslem  21978  ltbval  22021  opsrval  22024  psdmul  22132  mdetunilem1  22577  mdetunilem3  22579  mdetunilem4  22580  mdetunilem9  22585  chpscmat  22807  istopg  22860  isclo2  23053  neiptoptop  23096  neiptopnei  23097  lmbr  23223  ist0  23285  ist1-2  23312  t1sep2  23334  cmpfi  23373  2ndcdisj  23421  1stccn  23428  iskgen3  23514  ptpjopn  23577  hausdiag  23610  xkopt  23620  ist0-4  23694  isr0  23702  r0sep  23713  fbfinnfr  23806  fmfnfmlem2  23920  fmfnfmlem4  23922  fmfnfm  23923  cnflf  23967  cnfcf  24007  tmdgsum2  24061  tsmsf1o  24110  tsmsxplem1  24118  ustssel  24171  ustincl  24173  ustdiag  24174  ustinvel  24175  ustexhalf  24176  ust0  24185  ustuqtop4  24209  utopsnneiplem  24212  isucn2  24243  iducn  24247  metcnp  24506  txmetcnp  24512  metucn  24536  ngptgp  24601  nlmvscnlem1  24651  xrge0tsms  24800  xmetdcn2  24803  addcnlem  24830  ipcnlem1  25212  caucfil  25250  metcld  25273  metcld2  25274  ellimc2  25844  dvne0  25978  mdegleb  26029  mdegle0  26042  ply1divex  26102  fta1g  26135  dgrco  26240  plydivex  26263  fta1  26274  vieta1  26278  cxpcn3lem  26711  rlimcnp  26929  mpodvdsmulf1o  27157  dvdsmulf1o  27159  ppiublem1  27165  dchrinv  27224  lgseisenlem2  27339  2sqlem6  27386  2sqlem8  27389  2sqlem10  27391  nocvxminlem  27746  addsprop  27968  leadds1  27981  negsprop  28027  mulsprop  28122  bdayons  28268  onsfi  28348  expsne0  28428  istrkgc  28522  istrkgb  28523  axtgcgrid  28531  axtg5seg  28533  axtgpasch  28535  axtgeucl  28540  tgcgr4  28599  axlowdimlem15  29025  usgr2wlkneq  29824  usgr2pthlem  29831  friendshipgt3  30468  isnvlem  30681  vacn  30765  smcnlem  30768  norm3lemt  31223  isch2  31294  chlimi  31305  omlsii  31474  eigorth  31909  stcltr1i  32345  elat2  32411  funcnv5mpt  32740  xrge0infss  32833  sgn3da  32907  sgnnbi  32911  sgnpbi  32912  wrdt2ind  33013  xrge0tsmsd  33134  elrgspnlem4  33306  domnlcanOLD  33341  islinds5  33427  islbs5  33440  prmidlval  33497  rprmdvdspow  33593  1arithufdlem3  33606  evl1deg1  33636  evl1deg2  33637  evl1deg3  33638  ply1dg1rt  33640  ist0cld  33977  qqhucn  34136  esum2d  34237  eulerpartlemgvv  34520  tgoldbachgt  34807  axtgupdim2ALTV  34812  bnj1145  35135  bnj1171  35142  bnj1172  35143  tz9.1regs  35278  isacycgr1  35328  acycgrcycl  35329  erdszelem8  35380  satfrnmapom  35552  mclsval  35745  mclsax  35751  mclsppslem  35765  climuzcnv  35853  elintfv  35947  ifscgr  36226  idinside  36266  brsegle  36290  ixpeq12dv  36398  trer  36498  filnetlem4  36563  axtcond  36660  axuntco  36661  dfttc4lem1  36710  mh-setindnd  36719  mh-unprimbi  36726  mh-regprimbi  36727  mh-infprim2bi  36729  bj-ssblem1  36948  bj-ssblem2  36949  bj-ax12  36951  bj-19.21t0  37137  mobidvALT  37164  currysetlem  37252  currysetlem1  37254  wl-ax12v2cl  37822  wl-sbrimt  37872  fin2so  37928  ptrecube  37941  poimirlem26  37967  poimirlem27  37968  heicant  37976  mbfresfi  37987  itg2addnc  37995  filbcmb  38061  sdclem2  38063  fdc  38066  fdc1  38067  rngoidmlem  38257  divrngidl  38349  pridlval  38354  smprngopr  38373  inecmo  38676  elcnvrefrels3  38936  eldisjdmqsim2  39137  qmapeldisjsim  39181  rnqmapeleldisjsim  39183  disjlem18  39224  ax12inda  39394  ax12v2-o  39395  isat3  39753  iscvlat2N  39770  psubspset  40190  ldilfset  40554  ldilset  40555  dilfsetN  40598  dilsetN  40599  cdlemefrs29bpre0  40842  cdlemefrs29clN  40845  cdlemefrs32fva  40846  cdlemn11pre  41656  dihord2pre  41671  lpolsetN  41928  isprimroot  42532  primrootsunit1  42536  primrootscoprbij  42541  aks6d1c1  42555  hashscontpow  42561  sticksstones11  42595  sticksstones12a  42596  aks6d1c6lem3  42611  fimgmcyc  42979  fsuppind  43023  aomclem8  43489  hbtlem5  43556  unielss  43646  ifpbi1  43904  ifpbi12  43915  ifpbi13  43916  ntrneik2  44519  ntrneikb  44521  gneispacess2  44573  2sbc6g  44842  sbiota1  44861  relpeq2  45372  nregmodel  45444  uzwo4  45484  iineq12dv  45536  fsumiunss  46005  limsupre  46069  limsupref  46113  limsupbnd1f  46114  limsupmnf  46149  limsupre2  46153  limsupmnfuzlem  46154  limsupre2mpt  46158  limsupre3  46161  limsupre3mpt  46162  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvmptfprodlem  46372  wallispilem3  46495  fourierdlem48  46582  sge0f1o  46810  sge0iunmptlemre  46843  sge0iunmpt  46846  vonioo  47110  vonicc  47113  fcoresf1  47517  2reu8i  47561  2reuimp0  47562  2reuimp  47563  sprsymrelfolem2  47953  paireqne  47971  nfermltlrev  48220  bgoldbachlt  48289  tgoldbachlt  48292  gpgedgiov  48541  gpgedg2ov  48542  gpgedg2iv  48543  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem6  48600  pgnbgreunbgr  48601  ply1mulgsumlem1  48862  ply1mulgsumlem2  48863  elbigo2  49028  elbigo2r  49029  logic1  49266  postcposALT  50043  postc  50044  setrecseq  50160  setrec1lem1  50162  aacllem  50276