Theorem imbi1d 341

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  imbi12d  344  imbi1  347  imim21b  394  pm5.33  835  con3ALT  1084  norasslem3  1536  sbjust  2064  sbequ  2084  sb6  2086  19.21t  2207  sb4b  2480  drsb1  2500  cbvralsvw  3300  sbralie  3336  raleqf  3339  ralcom2  3361  rmoeq1  3400  rspceaimv  3612  ralxpxfr2d  3630  alexeqg  3635  elab6g  3653  mo2icl  3702  sbc19.21g  3842  csbiebg  3911  ralss  4038  ralssOLD  4040  r19.37zv  4482  reuprg0  4683  unissb  4920  intmin4  4958  dftr2c  5237  ssexg  5298  pocl  5574  vtoclr  5722  frsn  5747  cotrg  6101  dffun2  6546  fun11  6615  funimass4  6948  dff13  7252  f1mpt  7259  isopolem  7343  fnssintima  7360  oprabidw  7441  oprabid  7442  caovcan  7616  imaeqalov  7651  caoftrn  7717  ordunisuc2  7844  tfisi  7859  tfinds  7860  tfindsg  7861  tfindsg2  7862  dfom2  7868  findsg  7898  frxp  8130  xpord2indlem  8151  xpord3inddlem  8158  poseq  8162  frrlem12  8301  dfsmo2  8366  qliftfun  8821  ecoptocl  8826  ecopovtrn  8839  dom2lem  9011  findcard  9182  findcard2  9183  ssfi  9192  findcard3  9295  findcard3OLD  9296  fiint  9343  fiintOLD  9344  supmo  9469  eqsup  9473  suplub  9477  supisoex  9492  infmo  9514  wemaplem1  9565  wemaplem2  9566  wemapsolem  9569  oemapvali  9703  cantnf  9712  wemapwe  9716  ttrclss  9739  karden  9914  aceq1  10136  zorn2lem1  10515  axrepndlem2  10612  axregndlem2  10622  gruurn  10817  indpi  10926  nqereu  10948  prcdnq  11012  supexpr  11073  ltsosr  11113  supsrlem  11130  supsr  11131  axpre-lttrn  11185  axpre-sup  11188  prodgt0  12093  infm3  12206  prime  12679  raluz  12917  zsupss  12958  uzsupss  12961  xrsupsslem  13328  xrinfmsslem  13329  fz1sbc  13622  ssnn0fi  14008  fi1uzind  14530  brfi1indALT  14533  wrdind  14745  wrd2ind  14746  relexprelg  15062  rtrclreclem3  15084  relexpindlem  15087  relexpind  15088  rtrclind  15089  rexanre  15370  rexico  15377  reusq0  15486  limsupgle  15498  ello12  15537  ello12r  15538  ello1d  15544  elo12  15548  elo12r  15549  lo1resb  15585  o1resb  15587  rlimcn3  15611  addcn2  15615  mulcn2  15617  lo1le  15673  rpnnen2lem12  16248  sqrt2irr  16272  dfgcd2  16570  exprmfct  16728  isprm5  16731  isprm7  16732  prmdvdsexpr  16741  prmpwdvds  16929  vdwmc2  17004  ramtlecl  17025  ramub  17038  rami  17040  ramcl  17054  firest  17451  mreexexd  17665  acsfn  17676  prslem  18314  ispos  18331  posi  18334  isposd  18339  pospropd  18342  lubeldm  18368  lubval  18371  glbeldm  18381  glbval  18384  joinval2lem  18395  meetval2lem  18409  odlem1  19521  mndodcongi  19529  gexlem1  19565  sylow1lem3  19586  efgredlemb  19732  efgred  19734  frgpnabllem1  19859  isrrg  20663  isdomn4  20681  domnlcanb  20685  domnrcanb  20687  acsfn1p  20764  xrsdsreclb  21386  islindf4  21803  mplsubglem  21964  mpllsslem  21965  ltbval  22006  opsrval  22009  psdmul  22109  mdetunilem1  22555  mdetunilem3  22557  mdetunilem4  22558  mdetunilem9  22563  chpscmat  22785  istopg  22838  isclo2  23031  neiptoptop  23074  neiptopnei  23075  lmbr  23201  ist0  23263  ist1-2  23290  t1sep2  23312  cmpfi  23351  2ndcdisj  23399  1stccn  23406  iskgen3  23492  ptpjopn  23555  hausdiag  23588  xkopt  23598  ist0-4  23672  isr0  23680  r0sep  23691  fbfinnfr  23784  fmfnfmlem2  23898  fmfnfmlem4  23900  fmfnfm  23901  cnflf  23945  cnfcf  23985  tmdgsum2  24039  tsmsf1o  24088  tsmsxplem1  24096  ustssel  24149  ustincl  24151  ustdiag  24152  ustinvel  24153  ustexhalf  24154  ust0  24163  ustuqtop4  24188  utopsnneiplem  24191  isucn2  24222  iducn  24226  metcnp  24485  txmetcnp  24491  metucn  24515  ngptgp  24580  nlmvscnlem1  24630  xrge0tsms  24779  xmetdcn2  24782  addcnlem  24809  ipcnlem1  25202  caucfil  25240  metcld  25263  metcld2  25264  ellimc2  25835  dvne0  25973  mdegleb  26026  mdegle0  26039  ply1divex  26099  fta1g  26132  dgrco  26238  plydivex  26262  fta1  26273  vieta1  26277  cxpcn3lem  26714  rlimcnp  26932  mpodvdsmulf1o  27161  dvdsmulf1o  27163  ppiublem1  27170  dchrinv  27229  lgseisenlem2  27344  2sqlem6  27391  2sqlem8  27394  2sqlem10  27396  nocvxminlem  27746  addsprop  27940  sleadd1  27953  negsprop  27998  mulsprop  28090  bdayon  28230  onsfi  28304  expsne0  28378  istrkgc  28438  istrkgb  28439  axtgcgrid  28447  axtg5seg  28449  axtgpasch  28451  axtgeucl  28456  tgcgr4  28515  axlowdimlem15  28940  usgr2wlkneq  29743  usgr2pthlem  29750  friendshipgt3  30384  isnvlem  30596  vacn  30680  smcnlem  30683  norm3lemt  31138  isch2  31209  chlimi  31220  omlsii  31389  eigorth  31824  stcltr1i  32260  elat2  32326  funcnv5mpt  32651  xrge0infss  32742  sgn3da  32818  sgnnbi  32822  sgnpbi  32823  wrdt2ind  32934  resspos  32951  xrge0tsmsd  33061  elrgspnlem4  33245  domnlcanOLD  33279  islinds5  33387  islbs5  33400  prmidlval  33457  rprmdvdspow  33553  1arithufdlem3  33566  evl1deg1  33594  evl1deg2  33595  evl1deg3  33596  ply1dg1rt  33597  ist0cld  33869  qqhucn  34028  esum2d  34129  eulerpartlemgvv  34413  tgoldbachgt  34700  axtgupdim2ALTV  34705  bnj1145  35029  bnj1171  35036  bnj1172  35037  isacycgr1  35173  acycgrcycl  35174  erdszelem8  35225  satfrnmapom  35397  mclsval  35590  mclsax  35596  mclsppslem  35610  climuzcnv  35698  elintfv  35787  ifscgr  36067  idinside  36107  brsegle  36131  ixpeq12dv  36239  trer  36339  filnetlem4  36404  bj-ssblem1  36677  bj-ssblem2  36678  bj-ax12  36680  bj-19.21t0  36853  mobidvALT  36880  currysetlem  36968  currysetlem1  36970  wl-ax12v2cl  37529  wl-sbrimt  37570  fin2so  37636  ptrecube  37649  poimirlem26  37675  poimirlem27  37676  heicant  37684  mbfresfi  37695  itg2addnc  37703  filbcmb  37769  sdclem2  37771  fdc  37774  fdc1  37775  rngoidmlem  37965  divrngidl  38057  pridlval  38062  smprngopr  38081  inecmo  38378  elcnvrefrels3  38558  disjlem18  38823  ax12inda  38971  ax12v2-o  38972  isat3  39330  iscvlat2N  39347  psubspset  39768  ldilfset  40132  ldilset  40133  dilfsetN  40176  dilsetN  40177  cdlemefrs29bpre0  40420  cdlemefrs29clN  40423  cdlemefrs32fva  40424  cdlemn11pre  41234  dihord2pre  41249  lpolsetN  41506  isprimroot  42111  primrootsunit1  42115  primrootscoprbij  42120  aks6d1c1  42134  hashscontpow  42140  sticksstones11  42174  sticksstones12a  42175  aks6d1c6lem3  42190  fimgmcyc  42532  fsuppind  42588  aomclem8  43060  hbtlem5  43127  unielss  43217  ifpbi1  43476  ifpbi12  43487  ifpbi13  43488  ntrneik2  44091  ntrneikb  44093  gneispacess2  44145  2sbc6g  44414  sbiota1  44433  relpeq2  44945  nregmodel  45017  uzwo4  45057  iineq12dv  45110  fsumiunss  45584  limsupre  45650  limsupref  45694  limsupbnd1f  45695  limsupmnf  45730  limsupre2  45734  limsupmnfuzlem  45735  limsupre2mpt  45739  limsupre3  45742  limsupre3mpt  45743  ioodvbdlimc1lem2  45941  ioodvbdlimc2lem  45943  dvmptfprodlem  45953  wallispilem3  46076  fourierdlem48  46163  sge0f1o  46391  sge0iunmptlemre  46424  sge0iunmpt  46427  vonioo  46691  vonicc  46694  fcoresf1  47078  2reu8i  47122  2reuimp0  47123  2reuimp  47124  sprsymrelfolem2  47487  paireqne  47505  nfermltlrev  47738  bgoldbachlt  47807  tgoldbachlt  47810  ply1mulgsumlem1  48342  ply1mulgsumlem2  48343  elbigo2  48512  elbigo2r  48513  logic1  48750  postcposALT  49425  postc  49426  setrecseq  49529  setrec1lem1  49531  aacllem  49645