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  1537  sbjust  2066  sbequ  2086  sb6  2088  19.21t  2209  sb4b  2475  drsb1  2495  cbvralsvw  3283  sbralie  3318  raleqf  3321  ralcom2  3343  rmoeq1  3377  rspceaimv  3578  ralxpxfr2d  3596  alexeqg  3601  elab6g  3619  mo2icl  3668  sbc19.21g  3808  csbiebg  3877  ralss  4004  ralssOLD  4006  r19.37zv  4449  reuprg0  4652  unissb  4889  intmin4  4925  dftr2c  5199  ssexg  5259  pocl  5530  vtoclr  5677  frsn  5702  cotrg  6057  dffun2  6491  fun11  6555  funimass4  6886  dff13  7188  f1mpt  7195  isopolem  7279  fnssintima  7296  oprabidw  7377  oprabid  7378  caovcan  7550  imaeqalov  7585  caoftrn  7651  ordunisuc2  7774  tfisi  7789  tfinds  7790  tfindsg  7791  tfindsg2  7792  dfom2  7798  findsg  7827  frxp  8056  xpord2indlem  8077  xpord3inddlem  8084  poseq  8088  frrlem12  8227  dfsmo2  8267  qliftfun  8726  ecoptocl  8731  ecopovtrn  8744  dom2lem  8914  findcard  9073  findcard2  9074  ssfi  9082  findcard3  9167  fiint  9211  supmo  9336  eqsup  9340  suplub  9344  supisoex  9359  infmo  9381  wemaplem1  9432  wemaplem2  9433  wemapsolem  9436  oemapvali  9574  cantnf  9583  wemapwe  9587  ttrclss  9610  karden  9788  aceq1  10008  zorn2lem1  10387  axrepndlem2  10484  axregndlem2  10494  gruurn  10689  indpi  10798  nqereu  10820  prcdnq  10884  supexpr  10945  ltsosr  10985  supsrlem  11002  supsr  11003  axpre-lttrn  11057  axpre-sup  11060  prodgt0  11968  infm3  12081  prime  12554  raluz  12794  zsupss  12835  uzsupss  12838  xrsupsslem  13206  xrinfmsslem  13207  fz1sbc  13500  ssnn0fi  13892  fi1uzind  14414  brfi1indALT  14417  wrdind  14629  wrd2ind  14630  relexprelg  14945  rtrclreclem3  14967  relexpindlem  14970  relexpind  14971  rtrclind  14972  rexanre  15254  rexico  15261  reusq0  15372  limsupgle  15384  ello12  15423  ello12r  15424  ello1d  15430  elo12  15434  elo12r  15435  lo1resb  15471  o1resb  15473  rlimcn3  15497  addcn2  15501  mulcn2  15503  lo1le  15559  rpnnen2lem12  16134  sqrt2irr  16158  dfgcd2  16457  exprmfct  16615  isprm5  16618  isprm7  16619  prmdvdsexpr  16628  prmpwdvds  16816  vdwmc2  16891  ramtlecl  16912  ramub  16925  rami  16927  ramcl  16941  firest  17336  mreexexd  17554  acsfn  17565  prslem  18203  ispos  18220  posi  18223  isposd  18228  pospropd  18231  lubeldm  18257  lubval  18260  glbeldm  18270  glbval  18273  joinval2lem  18284  meetval2lem  18298  resspos  18335  odlem1  19447  mndodcongi  19455  gexlem1  19491  sylow1lem3  19512  efgredlemb  19658  efgred  19660  frgpnabllem1  19785  isrrg  20613  isdomn4  20631  domnlcanb  20635  domnrcanb  20637  acsfn1p  20714  xrsdsreclb  21350  islindf4  21775  mplsubglem  21936  mpllsslem  21937  ltbval  21978  opsrval  21981  psdmul  22081  mdetunilem1  22527  mdetunilem3  22529  mdetunilem4  22530  mdetunilem9  22535  chpscmat  22757  istopg  22810  isclo2  23003  neiptoptop  23046  neiptopnei  23047  lmbr  23173  ist0  23235  ist1-2  23262  t1sep2  23284  cmpfi  23323  2ndcdisj  23371  1stccn  23378  iskgen3  23464  ptpjopn  23527  hausdiag  23560  xkopt  23570  ist0-4  23644  isr0  23652  r0sep  23663  fbfinnfr  23756  fmfnfmlem2  23870  fmfnfmlem4  23872  fmfnfm  23873  cnflf  23917  cnfcf  23957  tmdgsum2  24011  tsmsf1o  24060  tsmsxplem1  24068  ustssel  24121  ustincl  24123  ustdiag  24124  ustinvel  24125  ustexhalf  24126  ust0  24135  ustuqtop4  24159  utopsnneiplem  24162  isucn2  24193  iducn  24197  metcnp  24456  txmetcnp  24462  metucn  24486  ngptgp  24551  nlmvscnlem1  24601  xrge0tsms  24750  xmetdcn2  24753  addcnlem  24780  ipcnlem1  25172  caucfil  25210  metcld  25233  metcld2  25234  ellimc2  25805  dvne0  25943  mdegleb  25996  mdegle0  26009  ply1divex  26069  fta1g  26102  dgrco  26208  plydivex  26232  fta1  26243  vieta1  26247  cxpcn3lem  26684  rlimcnp  26902  mpodvdsmulf1o  27131  dvdsmulf1o  27133  ppiublem1  27140  dchrinv  27199  lgseisenlem2  27314  2sqlem6  27361  2sqlem8  27364  2sqlem10  27366  nocvxminlem  27717  addsprop  27919  sleadd1  27932  negsprop  27977  mulsprop  28069  bdayon  28209  onsfi  28283  expsne0  28359  istrkgc  28432  istrkgb  28433  axtgcgrid  28441  axtg5seg  28443  axtgpasch  28445  axtgeucl  28450  tgcgr4  28509  axlowdimlem15  28934  usgr2wlkneq  29734  usgr2pthlem  29741  friendshipgt3  30378  isnvlem  30590  vacn  30674  smcnlem  30677  norm3lemt  31132  isch2  31203  chlimi  31214  omlsii  31383  eigorth  31818  stcltr1i  32254  elat2  32320  funcnv5mpt  32650  xrge0infss  32743  sgn3da  32817  sgnnbi  32821  sgnpbi  32822  wrdt2ind  32934  xrge0tsmsd  33042  elrgspnlem4  33212  domnlcanOLD  33246  islinds5  33332  islbs5  33345  prmidlval  33402  rprmdvdspow  33498  1arithufdlem3  33511  evl1deg1  33539  evl1deg2  33540  evl1deg3  33541  ply1dg1rt  33543  ist0cld  33846  qqhucn  34005  esum2d  34106  eulerpartlemgvv  34389  tgoldbachgt  34676  axtgupdim2ALTV  34681  bnj1145  35005  bnj1171  35012  bnj1172  35013  tz9.1regs  35130  isacycgr1  35190  acycgrcycl  35191  erdszelem8  35242  satfrnmapom  35414  mclsval  35607  mclsax  35613  mclsppslem  35627  climuzcnv  35715  elintfv  35809  ifscgr  36088  idinside  36128  brsegle  36152  ixpeq12dv  36260  trer  36360  filnetlem4  36425  bj-ssblem1  36698  bj-ssblem2  36699  bj-ax12  36701  bj-19.21t0  36874  mobidvALT  36901  currysetlem  36989  currysetlem1  36991  wl-ax12v2cl  37550  wl-sbrimt  37591  fin2so  37646  ptrecube  37659  poimirlem26  37685  poimirlem27  37686  heicant  37694  mbfresfi  37705  itg2addnc  37713  filbcmb  37779  sdclem2  37781  fdc  37784  fdc1  37785  rngoidmlem  37975  divrngidl  38067  pridlval  38072  smprngopr  38091  inecmo  38386  elcnvrefrels3  38626  disjlem18  38897  ax12inda  39046  ax12v2-o  39047  isat3  39405  iscvlat2N  39422  psubspset  39842  ldilfset  40206  ldilset  40207  dilfsetN  40250  dilsetN  40251  cdlemefrs29bpre0  40494  cdlemefrs29clN  40497  cdlemefrs32fva  40498  cdlemn11pre  41308  dihord2pre  41323  lpolsetN  41580  isprimroot  42185  primrootsunit1  42189  primrootscoprbij  42194  aks6d1c1  42208  hashscontpow  42214  sticksstones11  42248  sticksstones12a  42249  aks6d1c6lem3  42264  fimgmcyc  42626  fsuppind  42682  aomclem8  43153  hbtlem5  43220  unielss  43310  ifpbi1  43569  ifpbi12  43580  ifpbi13  43581  ntrneik2  44184  ntrneikb  44186  gneispacess2  44238  2sbc6g  44507  sbiota1  44526  relpeq2  45037  nregmodel  45109  uzwo4  45149  iineq12dv  45202  fsumiunss  45674  limsupre  45738  limsupref  45782  limsupbnd1f  45783  limsupmnf  45818  limsupre2  45822  limsupmnfuzlem  45823  limsupre2mpt  45827  limsupre3  45830  limsupre3mpt  45831  ioodvbdlimc1lem2  46029  ioodvbdlimc2lem  46031  dvmptfprodlem  46041  wallispilem3  46164  fourierdlem48  46251  sge0f1o  46479  sge0iunmptlemre  46512  sge0iunmpt  46515  vonioo  46779  vonicc  46782  fcoresf1  47168  2reu8i  47212  2reuimp0  47213  2reuimp  47214  sprsymrelfolem2  47592  paireqne  47610  nfermltlrev  47843  bgoldbachlt  47912  tgoldbachlt  47915  gpgedgiov  48164  gpgedg2ov  48165  gpgedg2iv  48166  pgnbgreunbgrlem1  48212  pgnbgreunbgrlem3  48217  pgnbgreunbgrlem4  48218  pgnbgreunbgrlem6  48223  pgnbgreunbgr  48224  ply1mulgsumlem1  48486  ply1mulgsumlem2  48487  elbigo2  48652  elbigo2r  48653  logic1  48890  postcposALT  49668  postc  49669  setrecseq  49785  setrec1lem1  49787  aacllem  49901