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  1099  norasslem3  1563  rename-sb  2096  sbequ  2123  sb6  2125  19.21t  2248  sb4b  2513  drsb1  2533  cbvralsvw  3322  sbralie  3349  raleqf  3352  ralcom2  3373  rmoeq1  3407  rspceaimv  3596  ralxpxfr2d  3614  alexeqg  3619  elab6g  3637  mo2icl  3686  sbc19.21g  3824  csbiebg  3893  ralss  4018  ralssOLD  4020  r19.37zv  4470  reuprg0  4670  unissb  4907  intmin4  4943  dftr2c  5222  ssexg  5291  pocl  5575  vtoclr  5722  frsn  5747  cotrg  6109  dffun2  6544  fun11  6608  funimass4  6943  dff13  7250  f1mpt  7257  isopolem  7341  fnssintima  7358  oprabidw  7439  oprabid  7440  caovcan  7612  imaeqalov  7647  caoftrn  7713  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  10476  axrepndlem2  10574  axregndlem2  10584  gruurn  10779  indpi  10888  nqereu  10910  prcdnq  10974  supexpr  11035  ltsosr  11075  supsrlem  11092  supsr  11093  axpre-lttrn  11147  axpre-sup  11150  prodgt0  12058  infm3  12170  prime  12673  raluz  12916  zsupss  12957  uzsupss  12960  xrsupsslem  13329  xrinfmsslem  13330  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  16277  sqrt2irr  16301  dfgcd2  16600  exprmfct  16759  isprm5  16762  isprm7  16763  prmdvdsexpr  16772  prmpwdvds  16960  vdwmc2  17035  ramtlecl  17056  ramub  17069  rami  17071  ramcl  17085  firest  17481  mreexexd  17700  acsfn  17711  prslem  18349  ispos  18366  posi  18369  isposd  18374  pospropd  18377  lubeldm  18403  lubval  18406  glbeldm  18416  glbval  18419  joinval2lem  18430  meetval2lem  18444  resspos  18481  odlem1  19601  mndodcongi  19609  gexlem1  19645  sylow1lem3  19666  efgredlemb  19812  efgred  19814  frgpnabllem1  19939  isrrg  20779  isdomn4  20796  domnlcanb  20800  domnrcanb  20802  acsfn1p  20876  prmidlval  21429  xrsdsreclb  21529  islindf4  21953  mplsubglem  22113  mpllsslem  22114  ltbval  22159  opsrval  22162  psdmul  22294  mdetunilem1  22734  mdetunilem3  22736  mdetunilem4  22737  mdetunilem9  22742  chpscmat  22964  istopg  23017  isclo2  23210  neiptoptop  23253  neiptopnei  23254  lmbr  23380  ist0  23442  ist1-2  23469  t1sep2  23491  cmpfi  23530  2ndcdisj  23578  1stccn  23585  iskgen3  23671  ptpjopn  23734  hausdiag  23767  xkopt  23777  ist0-4  23851  isr0  23859  r0sep  23870  fbfinnfr  23963  fmfnfmlem2  24077  fmfnfmlem4  24079  fmfnfm  24080  cnflf  24124  cnfcf  24164  tmdgsum2  24218  tsmsf1o  24267  tsmsxplem1  24275  ustssel  24328  ustincl  24330  ustdiag  24331  ustinvel  24332  ustexhalf  24333  ust0  24342  ustuqtop4  24366  utopsnneiplem  24369  isucn2  24400  iducn  24404  metcnp  24663  txmetcnp  24669  metucn  24693  ngptgp  24758  nlmvscnlem1  24808  xrge0tsms  24957  xmetdcn2  24960  addcnlem  24987  ipcnlem1  25369  caucfil  25407  metcld  25430  metcld2  25431  ellimc2  26001  dvne0  26135  mdegleb  26186  mdegle0  26199  ply1divex  26259  fta1g  26292  dgrco  26397  plydivex  26423  fta1  26434  vieta1  26438  cxpcn3lem  26874  rlimcnp  27092  mpodvdsmulf1o  27320  dvdsmulf1o  27322  ppiublem1  27328  dchrinv  27387  lgseisenlem2  27502  2sqlem6  27549  2sqlem8  27552  2sqlem10  27554  nocvxminlem  27909  addsprop  28131  leadds1  28144  negsprop  28190  mulsprop  28285  bdayons  28431  onsfi  28511  expsne0  28591  istrkgc  28685  istrkgb  28686  axtgcgrid  28694  axtg5seg  28696  axtgpasch  28698  axtgeucl  28703  tgcgr4  28762  axlowdimlem15  29243  usgr2wlkneq  30042  usgr2pthlem  30049  friendshipgt3  30686  isnvlem  30899  vacn  30983  smcnlem  30986  norm3lemt  31441  isch2  31512  chlimi  31523  omlsii  31692  eigorth  32127  stcltr1i  32563  elat2  32629  funcnv5mpt  32949  xrge0infss  33042  wrdt2ind  33210  xrge0tsmsd  33330  elrgspnlem4  33502  islinds5  33621  islbs5  33633  rprmdvdspow  33764  1arithufdlem3  33777  evl1deg1  33807  evl1deg2  33808  evl1deg3  33809  ply1dg1rt  33811  ist0cld  34164  qqhucn  34323  esum2d  34424  eulerpartlemgvv  34707  tgoldbachgt  34991  axtgupdim2ALTV  34996  bnj1145  35322  bnj1171  35329  bnj1172  35330  tz9.1regs  35466  isacycgr1  35533  acycgrcycl  35534  erdszelem8  35585  satfrnmapom  35757  mclsval  35950  mclsax  35956  mclsppslem  35970  climuzcnv  36058  elintfv  36152  ifscgr  36431  idinside  36471  brsegle  36495  ixpeq12dv  36613  trer  36712  filnetlem4  36777  axtcond  36874  axuntco  36875  dfttc4lem1  36924  mh-setindnd  36933  mh-unprimbi  36940  mh-regprimbi  36941  mh-infprim2bi  36943  bj-ssblem1  37161  bj-ssblem2  37162  bj-ax12  37164  bj-19.21t0  37350  mobidvALT  37377  currysetlem  37465  currysetlem1  37467  wl-ax12v2cl  38035  wl-sbrimt  38085  fin2so  38141  ptrecube  38154  poimirlem26  38180  poimirlem27  38181  heicant  38189  mbfresfi  38200  itg2addnc  38208  filbcmb  38274  sdclem2  38276  fdc  38279  fdc1  38280  rngoidmlem  38470  divrngidl  38562  pridlval  38567  smprngopr  38586  inecmo  38889  elcnvrefrels3  39149  eldisjdmqsim2  39350  qmapeldisjsim  39394  rnqmapeleldisjsim  39396  disjlem18  39437  ax12inda  39607  ax12v2-o  39608  isat3  39966  iscvlat2N  39983  psubspset  40403  ldilfset  40767  ldilset  40768  dilfsetN  40811  dilsetN  40812  cdlemefrs29bpre0  41055  cdlemefrs29clN  41058  cdlemefrs32fva  41059  cdlemn11pre  41869  dihord2pre  41884  lpolsetN  42141  isprimroot  42745  primrootsunit1  42749  primrootscoprbij  42754  aks6d1c1  42768  hashscontpow  42774  sticksstones11  42808  sticksstones12a  42809  aks6d1c6lem3  42824  fimgmcyc  43189  fsuppind  43209  aomclem8  43675  hbtlem5  43742  unielss  43832  ifpbi1  44090  ifpbi12  44101  ifpbi13  44102  ntrneik2  44705  ntrneikb  44707  gneispacess2  44759  2sbc6g  45012  sbiota1  45031  relpeq2  45541  nregmodel  45613  uzwo4  45660  iineq12dv  45711  fsumiunss  46178  limsupre  46242  limsupref  46286  limsupbnd1f  46287  limsupmnf  46322  limsupre2  46326  limsupmnfuzlem  46327  limsupre2mpt  46331  limsupre3  46334  limsupre3mpt  46335  ioodvbdlimc1lem2  46533  ioodvbdlimc2lem  46535  dvmptfprodlem  46545  wallispilem3  46668  fourierdlem48  46755  sge0f1o  46983  sge0iunmptlemre  47016  sge0iunmpt  47019  vonioo  47283  vonicc  47286  fcoresf1  47690  2reu8i  47734  2reuimp0  47735  2reuimp  47736  sprsymrelfolem2  48126  paireqne  48144  nfermltlrev  48393  bgoldbachlt  48462  tgoldbachlt  48465  gpgedgiov  48714  gpgedg2ov  48715  gpgedg2iv  48716  pgnbgreunbgrlem1  48762  pgnbgreunbgrlem3  48767  pgnbgreunbgrlem4  48768  pgnbgreunbgrlem6  48773  pgnbgreunbgr  48774  smprngprmrng  48988  ply1mulgsumlem1  49046  ply1mulgsumlem2  49047  elbigo2  49212  elbigo2r  49213  logic1  49449  postcposALT  50226  postc  50227  setrecseq  50343  setrec1lem1  50345  aacllem  50470