Theorem imbi1d 342

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 228	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
5	4	imim1d 82	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))
6	3, 5	impbid 211	1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  imbi12d  345  imbi1  348  imim21b  396  pm5.33  834  con3ALT  1085  norasslem3  1537  sbjust  2066  sbequ  2086  sb6  2088  19.21t  2199  sb4b  2474  sb4bOLD  2475  drsb1  2498  raleqf  3325  ralcom2  3347  rspceaimv  3578  ralxpxfr2d  3589  alexeqg  3594  elab6g  3614  mo2icl  3664  sbc19.21g  3809  csbiebg  3880  ralss  4006  r19.37zv  4451  reuprg0  4655  unissb  4892  intmin4  4930  dftr2c  5217  ssexg  5272  pocl  5544  poclOLD  5545  vtoclr  5686  frsn  5710  cotrg  6052  dffun2  6494  fun11  6563  funimass4  6895  dff13  7189  f1mpt  7195  isopolem  7277  fnssintima  7294  oprabidw  7373  oprabid  7374  caovcan  7543  caoftrn  7638  ordunisuc2  7763  tfisi  7778  tfinds  7779  tfindsg  7780  tfindsg2  7781  dfom2  7787  findsg  7819  frxp  8039  poseq  8050  frrlem12  8188  dfsmo2  8253  qliftfun  8667  ecoptocl  8672  ecopovtrn  8685  dom2lem  8858  findcard  9033  findcard2  9034  ssfi  9043  findcard2OLD  9154  findcard3  9155  findcard3OLD  9156  fiint  9194  supmo  9314  eqsup  9318  suplub  9322  supisoex  9336  infmo  9357  wemaplem1  9408  wemaplem2  9409  wemapsolem  9412  oemapvali  9546  cantnf  9555  wemapwe  9559  ttrclss  9582  karden  9757  aceq1  9979  zorn2lem1  10358  axrepndlem2  10455  axregndlem2  10465  pwfseqlem4  10524  gruurn  10660  indpi  10769  nqereu  10791  prcdnq  10855  supexpr  10916  ltsosr  10956  supsrlem  10973  supsr  10974  axpre-lttrn  11028  axpre-sup  11031  prodgt0  11928  infm3  12040  prime  12507  raluz  12742  zsupss  12783  uzsupss  12786  xrsupsslem  13147  xrinfmsslem  13148  fz1sbc  13438  ssnn0fi  13811  fi1uzind  14316  brfi1indALT  14319  wrdind  14534  wrd2ind  14535  relexprelg  14849  rtrclreclem3  14871  relexpindlem  14874  relexpind  14875  rtrclind  14876  rexanre  15158  rexico  15165  reusq0  15274  limsupgle  15286  ello12  15325  ello12r  15326  ello1d  15332  elo12  15336  elo12r  15337  lo1resb  15373  o1resb  15375  rlimcn3  15399  addcn2  15403  mulcn2  15405  lo1le  15463  rpnnen2lem12  16034  sqrt2irr  16058  dfgcd2  16354  exprmfct  16507  isprm5  16510  isprm7  16511  prmdvdsexpr  16520  prmpwdvds  16703  vdwmc2  16778  ramtlecl  16799  ramub  16812  rami  16814  ramcl  16828  firest  17241  mreexexd  17455  acsfn  17466  prslem  18114  ispos  18130  posi  18133  isposd  18139  pospropd  18143  lubeldm  18169  lubval  18172  glbeldm  18182  glbval  18185  joinval2lem  18196  meetval2lem  18210  odlem1  19240  mndodcongi  19248  gexlem1  19281  sylow1lem3  19302  efgredlemb  19448  efgred  19450  frgpnabllem1  19570  acsfn1p  20173  isrrg  20665  xrsdsreclb  20751  islindf4  21151  mplsubglem  21311  mpllsslem  21312  ltbval  21350  opsrval  21353  mdetunilem1  21867  mdetunilem3  21869  mdetunilem4  21870  mdetunilem9  21875  chpscmat  22097  istopg  22150  isclo2  22345  neiptoptop  22388  neiptopnei  22389  lmbr  22515  ist0  22577  ist1-2  22604  t1sep2  22626  cmpfi  22665  2ndcdisj  22713  1stccn  22720  iskgen3  22806  ptpjopn  22869  hausdiag  22902  xkopt  22912  ist0-4  22986  isr0  22994  r0sep  23005  fbfinnfr  23098  fmfnfmlem2  23212  fmfnfmlem4  23214  fmfnfm  23215  cnflf  23259  cnfcf  23299  tmdgsum2  23353  tsmsf1o  23402  tsmsxplem1  23410  ustssel  23463  ustincl  23465  ustdiag  23466  ustinvel  23467  ustexhalf  23468  ust0  23477  ustuqtop4  23502  utopsnneiplem  23505  isucn2  23537  iducn  23541  metcnp  23803  txmetcnp  23809  metucn  23833  ngptgp  23898  nlmvscnlem1  23956  xrge0tsms  24103  xmetdcn2  24106  addcnlem  24133  ipcnlem1  24515  caucfil  24553  metcld  24576  metcld2  24577  ellimc2  25147  dvne0  25281  mdegleb  25335  mdegle0  25348  ply1divex  25407  fta1g  25438  dgrco  25542  plydivex  25563  fta1  25574  vieta1  25578  cxpcn3lem  26006  rlimcnp  26221  dvdsmulf1o  26449  ppiublem1  26456  dchrinv  26515  lgseisenlem2  26630  2sqlem6  26677  2sqlem8  26680  2sqlem10  26682  nocvxminlem  27023  istrkgc  27104  istrkgb  27105  axtgcgrid  27113  axtg5seg  27115  axtgpasch  27117  axtgeucl  27122  tgcgr4  27181  axlowdimlem15  27613  usgr2wlkneq  28412  usgr2pthlem  28419  friendshipgt3  29050  isnvlem  29260  vacn  29344  smcnlem  29347  norm3lemt  29802  isch2  29873  chlimi  29884  omlsii  30053  eigorth  30488  stcltr1i  30924  elat2  30990  funcnv5mpt  31290  xrge0infss  31368  wrdt2ind  31510  resspos  31529  xrge0tsmsd  31602  islinds5  31858  prmidlval  31907  ist0cld  32079  qqhucn  32238  esum2d  32357  eulerpartlemgvv  32641  sgn3da  32806  sgnnbi  32810  sgnpbi  32811  tgoldbachgt  32941  axtgupdim2ALTV  32946  bnj1145  33270  bnj1171  33277  bnj1172  33278  isacycgr1  33405  acycgrcycl  33406  erdszelem8  33457  satfrnmapom  33629  mclsval  33822  mclsax  33828  mclsppslem  33842  climuzcnv  33926  imaeqalov  33981  elintfv  34022  xpord2ind  34076  xpord3ind  34082  addsprop  34240  sleadd1  34250  ifscgr  34483  idinside  34523  brsegle  34547  trer  34642  filnetlem4  34707  bj-ssblem1  34972  bj-ssblem2  34973  bj-ax12  34975  bj-19.21t0  35149  mobidvALT  35177  currysetlem  35270  currysetlem1  35272  wl-sbrimt  35859  fin2so  35918  ptrecube  35931  poimirlem26  35957  poimirlem27  35958  heicant  35966  mbfresfi  35977  itg2addnc  35985  filbcmb  36052  sdclem2  36054  fdc  36057  fdc1  36058  rngoidmlem  36248  divrngidl  36340  pridlval  36345  smprngopr  36364  inecmo  36670  elcnvrefrels3  36851  disjlem18  37116  ax12inda  37264  ax12v2-o  37265  isat3  37623  iscvlat2N  37640  psubspset  38061  ldilfset  38425  ldilset  38426  dilfsetN  38469  dilsetN  38470  cdlemefrs29bpre0  38713  cdlemefrs29clN  38716  cdlemefrs32fva  38717  cdlemn11pre  39527  dihord2pre  39542  lpolsetN  39799  sticksstones11  40418  sticksstones12a  40419  isdomn4  40478  fsuppind  40588  aomclem8  41198  hbtlem5  41265  ifpbi1  41456  ifpbi12  41467  ifpbi13  41468  ntrneik2  42073  ntrneikb  42075  gneispacess2  42127  2sbc6g  42404  sbiota1  42423  uzwo4  42971  fsumiunss  43502  limsupre  43568  limsupref  43612  limsupbnd1f  43613  limsupmnf  43648  limsupre2  43652  limsupmnfuzlem  43653  limsupre2mpt  43657  limsupre3  43660  limsupre3mpt  43661  ioodvbdlimc1lem2  43859  ioodvbdlimc2lem  43861  dvmptfprodlem  43871  wallispilem3  43994  fourierdlem48  44081  sge0f1o  44307  sge0iunmptlemre  44340  sge0iunmpt  44343  vonioo  44607  vonicc  44610  fcoresf1  44979  2reu8i  45021  2reuimp0  45022  2reuimp  45023  sprsymrelfolem2  45361  paireqne  45379  nfermltlrev  45612  bgoldbachlt  45681  tgoldbachlt  45684  ply1mulgsumlem1  46143  ply1mulgsumlem2  46144  elbigo2  46314  elbigo2r  46315  logic1  46552  postcposALT  46778  postc  46779  setrecseq  46807  setrec1lem1  46809  aacllem  46921