Theorem imbi1d 344

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 251	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	imim1d 83	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) → (𝜒 → 𝜃)))
4	1	biimpd 232	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
5	4	imim1d 83	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))
6	3, 5	impbid 215	1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  imbi12d  347  imbi1  350  imim21b  399  pm5.33  848  con3ALT  1101  norasslem3  1566  sbjust  2095  sbequ  2117  sb6  2119  19.21t  2242  sb4b  2507  drsb1  2527  cbvralsvw  3316  sbralie  3342  raleqf  3345  ralcom2  3366  rmoeq1  3400  rspceaimv  3587  ralxpxfr2d  3605  alexeqg  3610  elab6g  3628  mo2icl  3677  sbc19.21g  3815  csbiebg  3885  ralss  4010  ralssOLD  4012  r19.37zv  4468  reuprg0  4668  unissb  4906  intmin4  4942  dftr2c  5221  ssexgOLD  5294  pocl  5577  vtoclr  5724  frsn  5749  cotrg  6111  dffun2  6546  fun11  6610  funimass4  6945  dff13  7252  f1mpt  7259  isopolem  7343  fnssintima  7360  oprabidw  7441  oprabid  7442  caovcan  7614  imaeqalov  7649  caoftrn  7715  ordunisuc2  7836  tfisi  7851  tfinds  7852  tfindsg  7853  tfindsg2  7854  dfom2  7860  findsg  7890  frxp  8118  xpord2indlem  8139  xpord3inddlem  8146  poseq  8150  frrlem12  8290  dfsmo2  8330  qliftfun  8796  ecoptocl  8801  ecopovtrn  8814  dom2lem  8985  findcard  9144  findcard2  9145  ssfi  9153  findcard3  9239  fiint  9282  supmo  9408  eqsup  9412  suplub  9416  supisoex  9431  infmo  9453  wemaplem1  9504  wemaplem2  9505  wemapsolem  9508  oemapvali  9649  cantnf  9658  wemapwe  9662  ttrclss  9685  karden  9877  aceq1  10097  zorn2lem1  10475  axrepndlem2  10573  axregndlem2  10583  gruurn  10778  indpi  10887  nqereu  10909  prcdnq  10973  supexpr  11034  ltsosr  11074  supsrlem  11091  supsr  11092  axpre-lttrn  11146  axpre-sup  11149  prodgt0  12057  infm3  12169  prime  12672  raluz  12915  zsupss  12956  uzsupss  12959  xrsupsslem  13328  xrinfmsslem  13329  fz1sbc  13624  ssnn0fi  14017  fi1uzind  14540  brfi1indALT  14543  wrdind  14755  wrd2ind  14756  relexprelg  15071  rtrclreclem3  15093  relexpindlem  15096  relexpind  15097  rtrclind  15098  sgn3da  15134  sgnnbi  15137  sgnpbi  15138  rexanre  15394  rexico  15401  reusq0  15512  limsupgle  15524  ello12  15563  ello12r  15564  ello1d  15570  elo12  15574  elo12r  15575  lo1resb  15611  o1resb  15613  rlimcn3  15637  addcn2  15641  mulcn2  15643  lo1le  15699  rpnnen2lem12  16276  sqrt2irr  16300  dfgcd2  16599  exprmfct  16758  isprm5  16761  isprm7  16762  prmdvdsexpr  16771  prmpwdvds  16959  vdwmc2  17034  ramtlecl  17055  ramub  17068  rami  17070  ramcl  17084  firest  17480  mreexexd  17699  acsfn  17710  prslem  18348  ispos  18365  posi  18368  isposd  18373  pospropd  18376  lubeldm  18402  lubval  18405  glbeldm  18415  glbval  18418  joinval2lem  18429  meetval2lem  18443  resspos  18480  odlem1  19600  mndodcongi  19608  gexlem1  19644  sylow1lem3  19665  efgredlemb  19811  efgred  19813  frgpnabllem1  19938  isrrg  20797  isdomn4  20814  domnlcanb  20818  domnrcanb  20820  acsfn1p  20902  prmidlval  21462  xrsdsreclb  21564  islindf4  21988  mplsubglem  22148  mpllsslem  22149  ltbval  22194  opsrval  22197  psdmul  22329  mdetunilem1  22769  mdetunilem3  22771  mdetunilem4  22772  mdetunilem9  22777  chpscmat  22999  istopg  23052  isclo2  23245  neiptoptop  23288  neiptopnei  23289  lmbr  23415  ist0  23477  ist1-2  23504  t1sep2  23526  cmpfi  23565  2ndcdisj  23613  1stccn  23620  iskgen3  23706  ptpjopn  23769  hausdiag  23802  xkopt  23812  ist0-4  23886  isr0  23894  r0sep  23905  fbfinnfr  23998  fmfnfmlem2  24112  fmfnfmlem4  24114  fmfnfm  24115  cnflf  24159  cnfcf  24199  tmdgsum2  24253  tsmsf1o  24302  tsmsxplem1  24310  ustssel  24363  ustincl  24365  ustdiag  24366  ustinvel  24367  ustexhalf  24368  ust0  24377  ustuqtop4  24401  utopsnneiplem  24404  isucn2  24435  iducn  24439  metcnp  24698  txmetcnp  24704  metucn  24728  ngptgp  24793  nlmvscnlem1  24843  xrge0tsms  24992  xmetdcn2  24995  addcnlem  25022  ipcnlem1  25404  caucfil  25442  metcld  25465  metcld2  25466  ellimc2  26036  dvne0  26170  mdegleb  26221  mdegle0  26234  ply1divex  26294  fta1g  26327  dgrco  26432  plydivex  26458  fta1  26469  vieta1  26473  cxpcn3lem  26912  rlimcnp  27130  mpodvdsmulf1o  27358  dvdsmulf1o  27360  ppiublem1  27366  dchrinv  27425  lgseisenlem2  27540  2sqlem6  27587  2sqlem8  27590  2sqlem10  27592  nocvxminlem  27947  addsprop  28169  leadds1  28182  negsprop  28228  mulsprop  28323  bdayons  28469  onsfi  28549  expsne0  28629  istrkgc  28723  istrkgb  28724  axtgcgrid  28732  axtg5seg  28734  axtgpasch  28736  axtgeucl  28741  tgcgr4  28800  axlowdimlem15  29306  usgr2wlkneq  30105  usgr2pthlem  30112  friendshipgt3  30749  isnvlem  30962  vacn  31046  smcnlem  31049  norm3lemt  31504  isch2  31575  chlimi  31586  omlsii  31755  eigorth  32190  stcltr1i  32626  elat2  32692  funcnv5mpt  33012  xrge0infss  33105  wrdt2ind  33273  xrge0tsmsd  33393  elrgspnlem4  33565  islinds5  33682  islbs5  33693  rprmdvdspow  33823  1arithufdlem3  33836  evl1deg1  33866  evl1deg2  33867  evl1deg3  33868  ply1dg1rt  33870  ist0cld  34223  qqhucn  34382  esum2d  34483  eulerpartlemgvv  34766  tgoldbachgt  35050  axtgupdim2ALTV  35055  bnj1145  35381  bnj1171  35388  bnj1172  35389  tz9.1regs  35547  isacycgr1  35638  acycgrcycl  35639  erdszelem8  35690  satfrnmapom  35862  mclsval  36055  mclsax  36061  mclsppslem  36075  climuzcnv  36163  elintfv  36257  ifscgr  36536  idinside  36576  brsegle  36600  ixpeq12dv  36728  trer  36827  filnetlem4  36892  axtcond  36989  axuntco  36990  dfttc4lem1  37039  mh-setindnd  37048  mh-unprimbi  37055  mh-regprimbi  37056  mh-infprim2bi  37058  bj-ssblem1  37276  bj-ssblem2  37277  bj-ax12  37279  bj-19.21t0  37465  mobidvALT  37492  currysetlem  37581  currysetlem1  37583  wl-ax12v2cl  38152  wl-sbrimt  38202  fin2so  38258  ptrecube  38271  poimirlem26  38297  poimirlem27  38298  heicant  38306  mbfresfi  38317  itg2addnc  38325  filbcmb  38391  sdclem2  38393  fdc  38396  fdc1  38397  rngoidmlem  38587  divrngidl  38679  pridlval  38684  smprngopr  38703  inecmo  39004  elcnvrefrels3  39264  eldisjdmqsim2  39465  qmapeldisjsim  39509  rnqmapeleldisjsim  39511  disjlem18  39552  ax12inda  39722  ax12v2-o  39723  isat3  40081  iscvlat2N  40098  psubspset  40518  ldilfset  40882  ldilset  40883  dilfsetN  40926  dilsetN  40927  cdlemefrs29bpre0  41170  cdlemefrs29clN  41173  cdlemefrs32fva  41174  cdlemn11pre  41984  dihord2pre  41999  lpolsetN  42256  isprimroot  42860  primrootsunit1  42864  primrootscoprbij  42869  aks6d1c1  42883  hashscontpow  42889  sticksstones11  42923  sticksstones12a  42924  aks6d1c6lem3  42939  fimgmcyc  43302  fsuppind  43322  aomclem8  43788  hbtlem5  43855  unielss  43945  ifpbi1  44203  ifpbi12  44214  ifpbi13  44215  ntrneik2  44818  ntrneikb  44820  gneispacess2  44872  2sbc6g  45125  sbiota1  45144  relpeq2  45654  nregmodel  45726  uzwo4  45773  iineq12dv  45824  fsumiunss  46291  limsupre  46355  limsupref  46399  limsupbnd1f  46400  limsupmnf  46435  limsupre2  46439  limsupmnfuzlem  46440  limsupre2mpt  46444  limsupre3  46447  limsupre3mpt  46448  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  dvmptfprodlem  46658  wallispilem3  46781  fourierdlem48  46868  sge0f1o  47096  sge0iunmptlemre  47129  sge0iunmpt  47132  vonioo  47396  vonicc  47399  fcoresf1  47806  2reu8i  47850  2reuimp0  47851  2reuimp  47852  sprsymrelfolem2  48242  paireqne  48260  nfermltlrev  48509  bgoldbachlt  48578  tgoldbachlt  48581  gpgedgiov  48830  gpgedg2ov  48831  gpgedg2iv  48832  pgnbgreunbgrlem1  48878  pgnbgreunbgrlem3  48883  pgnbgreunbgrlem4  48884  pgnbgreunbgrlem6  48889  pgnbgreunbgr  48890  smprngprmrng  49104  ply1mulgsumlem1  49166  ply1mulgsumlem2  49167  elbigo2  49332  elbigo2r  49333  logic1  49569  postcposALT  50346  postc  50347  setrecseq  50463  setrec1lem1  50465  aacllem  50621