Theorem imbi1d 330

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 237	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	imim1d 80	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) → (𝜒 → 𝜃)))
4	1	biimpd 218	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
5	4	imim1d 80	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))
6	3, 5	impbid 201	1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  imbi12d  333  imbi1  336  imim21b  381  pm5.33  918  con3ALT  1026  con3OLD  1029  19.21t  2061  19.21tOLD  2201  axc15  2291  ax12v2OLD  2330  drsb1  2365  ralcom2  3083  raleqf  3111  ralxpxfr2d  3298  alexeqg  3302  mo2icl  3352  sbc19.21g  3469  csbiebg  3522  ralss  3631  r19.37zv  4019  ssuniOLD  4396  intmin4  4441  ssexg  4732  pocl  4966  vtoclr  5086  frsn  5112  fun11  5877  funimass4  6157  dff13  6416  f1mpt  6419  isopolem  6495  oprabid  6576  caovcan  6736  caoftrn  6830  ordunisuc2  6936  tfisi  6950  tfinds  6951  tfindsg  6952  tfindsg2  6953  dfom2  6959  findsg  6985  frxp  7174  dfsmo2  7331  qliftfun  7719  ecoptocl  7724  ecopovtrn  7737  dom2lem  7881  findcard  8084  findcard2  8085  findcard3  8088  fiint  8122  supmo  8241  eqsup  8245  suplub  8249  supisoex  8263  infmo  8284  wemaplem1  8334  wemaplem2  8335  wemapsolem  8338  oemapvali  8464  cantnf  8473  wemapwe  8477  karden  8641  aceq1  8823  zorn2lem1  9201  axrepndlem2  9294  axregndlem2  9304  pwfseqlem4  9363  gruurn  9499  indpi  9608  nqereu  9630  prcdnq  9694  supexpr  9755  ltsosr  9794  supsrlem  9811  supsr  9812  axpre-lttrn  9866  axpre-sup  9869  prodgt0  10747  infm3  10861  prime  11334  raluz  11612  zsupss  11653  uzsupss  11656  xrsupsslem  12009  xrinfmsslem  12010  fz1sbc  12285  ssnn0fi  12646  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  wrdind  13328  wrd2ind  13329  relexprelg  13626  rtrclreclem3  13648  relexpindlem  13651  relexpind  13652  rtrclind  13653  rexanre  13934  rexico  13941  limsupgle  14056  rlim2lt  14076  rlim3  14077  ello12  14095  ello12r  14096  ello1d  14102  elo12  14106  elo12r  14107  rlimconst  14123  lo1resb  14143  o1resb  14145  rlimcn2  14169  addcn2  14172  mulcn2  14174  reccn2  14175  cn1lem  14176  o1rlimmul  14197  lo1le  14230  caucvgrlem  14251  divrcnv  14423  rpnnen2lem12  14793  sqrt2irr  14817  dfgcd2  15101  exprmfct  15254  isprm5  15257  isprm7  15258  prmdvdsexpr  15267  prmpwdvds  15446  vdwmc2  15521  ramtlecl  15542  ramub  15555  rami  15557  ramcl  15571  firest  15916  mreexexd  16131  mreexexdOLD  16132  acsfn  16143  prslem  16754  ispos  16770  posi  16773  isposd  16778  lubeldm  16804  lubval  16807  glbeldm  16817  glbval  16820  joinval2lem  16831  meetval2lem  16845  pospropd  16957  odlem1  17777  mndodcongi  17785  gexlem1  17817  sylow1lem3  17838  efgredlemb  17982  efgred  17984  frgpnabllem1  18099  isrrg  19109  mplsubglem  19255  mpllsslem  19256  ltbval  19292  opsrval  19295  xrsdsreclb  19612  islindf4  19996  mdetunilem1  20237  mdetunilem3  20239  mdetunilem4  20240  mdetunilem9  20245  chpscmat  20466  chfacffsupp  20480  chfacfscmulfsupp  20483  chfacfpmmulfsupp  20487  istopg  20525  isclo2  20702  neiptoptop  20745  neiptopnei  20746  lmbr  20872  ist0  20934  ist1-2  20961  t1sep2  20983  cmpfi  21021  2ndcdisj  21069  1stccn  21076  iskgen3  21162  ptpjopn  21225  hausdiag  21258  xkopt  21268  ist0-4  21342  isr0  21350  r0sep  21361  fbfinnfr  21455  fmfnfmlem2  21569  fmfnfmlem4  21571  fmfnfm  21572  cnflf  21616  cnfcf  21656  tmdgsum2  21710  tsmsgsum  21752  tsmsres  21757  tsmsf1o  21758  tsmsxplem1  21766  tsmsxp  21768  ustssel  21819  ustincl  21821  ustdiag  21822  ustinvel  21823  ustexhalf  21824  ust0  21833  ustuqtop4  21858  utopsnneiplem  21861  isucn2  21893  iducn  21897  metcnp  22156  metcnpi3  22161  txmetcnp  22162  metucn  22186  ngptgp  22250  nlmvscnlem1  22300  nrginvrcnlem  22305  nghmcn  22359  xrge0tsms  22445  xmetdcn2  22448  metdscn  22467  addcnlem  22475  elcncf1di  22506  ipcnlem1  22852  caucfil  22889  metcld  22912  metcld2  22913  volcn  23180  itg2cnlem2  23335  ellimc2  23447  dveflem  23546  dvne0  23578  mdegleb  23628  mdegle0  23641  ply1divex  23700  fta1g  23731  dgrco  23835  plydivex  23856  fta1  23867  vieta1  23871  abelthlem8  23997  divlogrlim  24181  cxpcn3lem  24288  rlimcnp  24492  cxplim  24498  cxploglim  24504  ftalem1  24599  ftalem2  24600  dvdsmulf1o  24720  ppiublem1  24727  dchrinv  24786  lgseisenlem2  24901  2sqlem6  24948  2sqlem8  24951  2sqlem10  24953  dchrisum0  25009  istrkgc  25153  istrkgb  25154  axtgcgrid  25162  axtg5seg  25164  axtgpasch  25166  axtgeucl  25171  tgcgr4  25226  axlowdimlem15  25636  usgra2wlkspthlem1  26147  usgra2wlkspthlem2  26148  3v3e3cycl1  26172  constr3trllem2  26179  4cycl4v4e  26194  4cycl4dv4e  26196  eupatrl  26495  frgrawopreglem2  26572  usg2spot2nb  26592  friendshipgt3  26648  isnvlem  26849  vacn  26933  nmcvcn  26934  smcnlem  26936  blocni  27044  norm3lemt  27393  isch2  27464  chlimi  27475  omlsii  27646  eigorth  28081  0cnop  28222  0cnfn  28223  idcnop  28224  lnconi  28276  stcltr1i  28517  elat2  28583  funcnv5mpt  28852  xrge0infss  28915  resspos  28990  xrge0tsmsd  29116  qqhcn  29363  qqhucn  29364  esum2d  29482  eulerpartlemgvv  29765  sgn3da  29930  sgnnbi  29934  sgnpbi  29935  axtgupdim2OLD  29999  bnj1145  30315  bnj1171  30322  bnj1172  30323  erdszelem8  30434  mclsval  30714  mclsax  30720  mclsppslem  30734  climuzcnv  30819  poseq  30994  frrlem4  31027  nocvxminlem  31089  ifscgr  31321  idinside  31361  brsegle  31385  trer  31480  filnetlem4  31546  dnicn  31652  bj-ssbequ  31818  bj-ssblem1  31819  bj-ssblem2  31820  bj-ssb1a  31821  bj-ssb1  31822  bj-ssbcom3lem  31839  bj-19.21t  32005  wl-sbrimt  32510  fin2so  32566  ptrecube  32579  poimirlem26  32605  poimirlem27  32606  heicant  32614  mbfresfi  32626  itg2addnc  32634  ftc1anc  32663  filbcmb  32705  sdclem2  32708  fdc  32711  fdc1  32712  rngoidmlem  32905  divrngidl  32997  pridlval  33002  smprngopr  33021  ax12inda  33251  ax12v2-o  33252  isat3  33612  iscvlat2N  33629  psubspset  34048  ldilfset  34412  ldilset  34413  dilfsetN  34457  dilsetN  34458  cdlemefrs29bpre0  34702  cdlemefrs29clN  34705  cdlemefrs32fva  34706  cdlemn11pre  35517  dihord2pre  35532  lpolsetN  35789  aomclem8  36649  hbtlem5  36717  acsfn1p  36788  ifpbi1  36841  ifpbi12  36852  ifpbi13  36853  ntrneik2  37410  ntrneikb  37412  gneispacess2  37464  2sbc6g  37638  sbiota1  37657  uzwo4  38246  fsumiunss  38642  mullimc  38683  limcdm0  38685  mullimcf  38690  constlimc  38691  idlimc  38693  limsupre  38708  limcleqr  38711  addlimc  38715  0ellimcdiv  38716  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvmptfprodlem  38834  wallispilem3  38960  fourierdlem48  39047  fourierdlem87  39086  sge0f1o  39275  sge0iunmptlemre  39308  sge0iunmpt  39311  vonioo  39573  vonicc  39576  bgoldbachlt  40227  tgoldbachlt  40230  bgoldbachltOLD  40234  tgoldbachltOLD  40237  usgr2wlkneq  40962  usgr2pthlem  40969  av-friendshipgt3  41552  ply1mulgsumlem1  41968  ply1mulgsumlem2  41969  elbigo2  42144  elbigo2r  42145  setrecseq  42231  setrec1lem1  42233  aacllem  42356