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 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  imbi12d  347  imbi1  350  imim21b  400  pm5.33  849  con3ALT  1101  norasslem3  1566  sbjust  2098  sbequ  2120  sb6  2122  19.21t  2242  sb4b  2504  drsb1  2524  cbvralsvw  3313  sbralie  3338  raleqf  3341  ralcom2  3362  rmoeq1  3396  rspceaimv  3582  ralxpxfr2d  3600  alexeqg  3605  elab6g  3623  mo2icl  3672  sbc19.21g  3810  csbiebg  3879  ralss  4004  ralssOLD  4006  r19.37zv  4463  reuprg0  4663  unissb  4901  intmin4  4937  dftr2c  5215  ssexgOLD  5288  pocl  5571  vtoclr  5718  frsn  5743  cotrg  6105  dffun2  6543  fun11  6607  funimass4  6942  dff13  7251  f1mpt  7258  isopolem  7346  fnssintima  7365  oprabidw  7444  oprabid  7445  caovcan  7618  imaeqalov  7653  caoftrn  7719  ordunisuc2  7840  tfisi  7855  tfinds  7856  tfindsg  7857  tfindsg2  7858  dfom2  7864  findsg  7894  frxp  8124  xpord2indlem  8145  xpord3inddlem  8152  poseq  8156  frrlem12  8296  dfsmo2  8336  qliftfun  8802  ecoptocl  8807  ecopovtrn  8820  dom2lem  8998  findcard  9158  findcard2  9159  ssfi  9167  findcard3  9253  fiint  9296  supmo  9422  eqsup  9426  suplub  9430  supisoex  9445  infmo  9467  wemaplem1  9518  wemaplem2  9519  wemapsolem  9522  oemapvali  9663  cantnf  9672  wemapwe  9676  ttrclss  9699  kardenOLD  9899  aceq1  10120  zorn2lem1  10498  axrepndlem2  10602  axregndlem2  10612  gruurn  10807  indpi  10916  nqereu  10938  prcdnq  11002  supexpr  11063  ltsosr  11103  supsrlem  11120  supsr  11121  axpre-lttrn  11175  axpre-sup  11178  prodgt0  12086  infm3  12198  prime  12702  raluz  12945  zsupss  12986  uzsupss  12989  xrsupsslem  13359  xrinfmsslem  13360  fz1sbc  13655  ssnn0fi  14049  fi1uzind  14572  brfi1indALT  14575  wrdind  14791  wrd2ind  14792  relexprelg  15111  rtrclreclem3  15133  relexpindlem  15136  relexpind  15137  rtrclind  15138  sgn3da  15174  sgnnbi  15177  sgnpbi  15178  rexanre  15434  rexico  15441  reusq0  15552  limsupgle  15564  ello12  15603  ello12r  15604  ello1d  15610  elo12  15614  elo12r  15615  lo1resb  15651  o1resb  15653  rlimcn3  15677  addcn2  15681  mulcn2  15683  lo1le  15739  rpnnen2lem12  16313  sqrt2irr  16337  dfgcd2  16636  exprmfct  16795  isprm5  16798  isprm7  16799  prmdvdsexpr  16808  prmpwdvds  16996  vdwmc2  17071  ramtlecl  17092  ramub  17105  rami  17107  ramcl  17121  firest  17517  mreexexd  17736  acsfn  17747  prslem  18385  ispos  18402  posi  18405  isposd  18410  pospropd  18413  lubeldm  18439  lubval  18442  glbeldm  18452  glbval  18455  joinval2lem  18466  meetval2lem  18480  resspos  18517  odlem1  19662  mndodcongi  19670  gexlem1  19706  sylow1lem3  19727  efgredlemb  19873  efgred  19875  frgpnabllem1  20000  isrrg  20860  isdomn4  20877  domnlcanb  20881  domnrcanb  20883  acsfn1p  20965  prmidlval  21525  xrsdsreclb  21627  islindf4  22051  mplsubglem  22213  mpllsslem  22214  ltbval  22259  opsrval  22262  psdmul  22394  mdetunilem1  22834  mdetunilem3  22836  mdetunilem4  22837  mdetunilem9  22842  chpscmat  23067  istopg  23120  isclo2  23313  neiptoptop  23356  neiptopnei  23357  lmbr  23483  ist0  23545  ist1-2  23572  t1sep2  23594  cmpfi  23633  2ndcdisj  23682  1stccn  23689  iskgen3  23775  ptpjopn  23838  hausdiag  23871  xkopt  23881  ist0-4  23955  isr0  23963  r0sep  23974  fbfinnfr  24067  fmfnfmlem2  24181  fmfnfmlem4  24183  fmfnfm  24184  cnflf  24228  cnfcf  24268  tmdgsum2  24322  tsmsf1o  24371  tsmsxplem1  24379  ustssel  24432  ustincl  24434  ustdiag  24435  ustinvel  24436  ustexhalf  24437  ust0  24446  ustuqtop4  24470  utopsnneiplem  24473  isucn2  24504  iducn  24508  metcnp  24767  txmetcnp  24773  metucn  24797  ngptgp  24862  nlmvscnlem1  24912  xrge0tsms  25061  xmetdcn2  25064  addcnlem  25091  ipcnlem1  25473  caucfil  25511  metcld  25534  metcld2  25535  ellimc2  26104  dvne0  26238  mdegleb  26289  mdegle0  26302  ply1divex  26362  fta1g  26395  dgrco  26501  plydivex  26527  fta1  26538  vieta1  26544  cxpcn3lem  26984  rlimcnp  27202  mpodvdsmulf1o  27430  dvdsmulf1o  27432  ppiublem1  27438  dchrinv  27497  lgseisenlem2  27612  2sqlem6  27659  2sqlem8  27662  2sqlem10  27664  nocvxminlem  28019  addsprop  28241  leadds1  28254  negsprop  28300  mulsprop  28395  bdayons  28541  onsfi  28621  expsne0  28701  istrkgc  28795  istrkgb  28796  axtgcgrid  28804  axtg5seg  28806  axtgpasch  28808  axtgeucl  28813  tgcgr4  28873  axlowdimlem15  29413  usgr2wlkneq  30221  usgr2pthlem  30228  isacycgr1  30631  acycgrcycl  30632  friendshipgt3  30878  isnvlem  31091  vacn  31175  smcnlem  31178  norm3lemt  31633  isch2  31704  chlimi  31715  omlsii  31884  eigorth  32319  stcltr1i  32755  elat2  32821  funcnv5mpt  33140  xrge0infss  33231  wrdt2ind  33395  xrge0tsmsd  33513  elrgspnlem4  33685  islinds5  33802  islbs5  33813  rprmdvdspow  33943  1arithufdlem3  33956  evl1deg1  33986  evl1deg2  33987  evl1deg3  33988  ply1dg1rt  33990  ist0cld  34343  qqhucn  34502  esum2d  34603  eulerpartlemgvv  34887  tgoldbachgt  35171  axtgupdim2ALTV  35176  bnj1145  35502  bnj1171  35509  bnj1172  35510  tz9.1regs  35660  erdszelem8  35777  satfrnmapom  35949  mclsval  36142  mclsax  36148  mclsppslem  36162  climuzcnv  36250  elintfv  36344  ifscgr  36624  idinside  36664  brsegle  36688  ixpeq12dv  36836  trer  36935  filnetlem4  37000  axtcond  37097  axuntco  37098  dfttc4lem1  37147  mh-setindnd  37156  mh-unprimbi  37163  mh-regprimbi  37164  mh-infprim2bi  37166  bj-ssblem1  37384  bj-ssblem2  37385  bj-ax12  37387  bj-19.21t0  37573  mobidvALT  37600  currysetlem  37689  currysetlem1  37691  wl-ax12v2cl  38260  wl-sbrimt  38310  fin2so  38361  ptrecube  38369  poimirlem26  38395  poimirlem27  38396  heicant  38404  mbfresfi  38415  itg2addnc  38423  findcard4  38463  filbcmb  38490  sdclem2  38492  fdc  38495  fdc1  38496  rngoidmlem  38686  divrngidl  38778  pridlval  38783  smprngopr  38802  inecmo  39103  elcnvrefrels3  39363  eldisjdmqsim2  39564  qmapeldisjsim  39608  rnqmapeleldisjsim  39610  disjlem18  39651  ax12inda  39821  ax12v2-o  39822  isat3  40180  iscvlat2N  40197  psubspset  40617  ldilfset  40981  ldilset  40982  dilfsetN  41025  dilsetN  41026  cdlemefrs29bpre0  41269  cdlemefrs29clN  41272  cdlemefrs32fva  41273  cdlemn11pre  42083  dihord2pre  42098  lpolsetN  42355  isprimroot  42959  primrootsunit1  42963  primrootscoprbij  42968  aks6d1c1  42982  hashscontpow  42988  sticksstones11  43022  sticksstones12a  43023  aks6d1c6lem3  43038  fimgmcyc  43416  fsuppind  43436  aomclem8  43902  hbtlem5  43969  unielss  44059  ifpbi1  44317  ifpbi12  44328  ifpbi13  44329  ntrneik2  44932  ntrneikb  44934  gneispacess2  44986  2sbc6g  45239  sbiota1  45258  relpeq2  45768  nregmodel  45840  uzwo4  45887  iineq12dv  45938  fsumiunss  46405  limsupre  46469  limsupref  46513  limsupbnd1f  46514  limsupmnf  46549  limsupre2  46553  limsupmnfuzlem  46554  limsupre2mpt  46558  limsupre3  46561  limsupre3mpt  46562  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  dvmptfprodlem  46772  wallispilem3  46895  fourierdlem48  46982  sge0f1o  47210  sge0iunmptlemre  47243  sge0iunmpt  47246  vonioo  47510  vonicc  47513  fcoresf1  47957  2reu8i  48001  2reuimp0  48002  2reuimp  48003  sprsymrelfolem2  48393  paireqne  48411  nfermltlrev  48660  bgoldbachlt  48729  tgoldbachlt  48732  gpgedgiov  48981  gpgedg2ov  48982  gpgedg2iv  48983  pgnbgreunbgrlem1  49029  pgnbgreunbgrlem3  49034  pgnbgreunbgrlem4  49035  pgnbgreunbgrlem6  49040  pgnbgreunbgr  49041  smprngprmrng  49254  ply1mulgsumlem1  49316  ply1mulgsumlem2  49317  elbigo2  49482  elbigo2r  49483  logic1  49719  postcposALT  50494  postc  50495  setrecseq  50611  setrec1lem1  50613  aacllem  50772