Theorem imbi1d 340

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 247	. . 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  343  imbi1  346  imim21b  393  pm5.33  832  con3ALT  1083  norasslem3  1535  sbjust  2064  sbequ  2084  sb6  2086  19.21t  2197  sb4b  2472  drsb1  2492  raleqf  3347  ralcom2  3371  rmoeq1  3412  rspceaimv  3618  ralxpxfr2d  3635  alexeqg  3640  elab6g  3660  mo2icl  3711  sbc19.21g  3856  csbiebg  3927  ralss  4055  r19.37zv  4502  reuprg0  4707  unissb  4944  intmin4  4982  dftr2c  5269  ssexg  5324  pocl  5596  poclOLD  5597  vtoclr  5740  frsn  5764  cotrg  6109  dffun2  6554  fun11  6623  funimass4  6957  dff13  7258  f1mpt  7264  isopolem  7346  fnssintima  7363  oprabidw  7444  oprabid  7445  caovcan  7615  imaeqalov  7650  caoftrn  7712  ordunisuc2  7837  tfisi  7852  tfinds  7853  tfindsg  7854  tfindsg2  7855  dfom2  7861  findsg  7894  frxp  8116  xpord2indlem  8137  xpord3inddlem  8144  poseq  8148  frrlem12  8286  dfsmo2  8351  qliftfun  8800  ecoptocl  8805  ecopovtrn  8818  dom2lem  8992  findcard  9167  findcard2  9168  ssfi  9177  findcard2OLD  9288  findcard3  9289  findcard3OLD  9290  fiint  9328  supmo  9451  eqsup  9455  suplub  9459  supisoex  9473  infmo  9494  wemaplem1  9545  wemaplem2  9546  wemapsolem  9549  oemapvali  9683  cantnf  9692  wemapwe  9696  ttrclss  9719  karden  9894  aceq1  10116  zorn2lem1  10495  axrepndlem2  10592  axregndlem2  10602  pwfseqlem4  10661  gruurn  10797  indpi  10906  nqereu  10928  prcdnq  10992  supexpr  11053  ltsosr  11093  supsrlem  11110  supsr  11111  axpre-lttrn  11165  axpre-sup  11168  prodgt0  12067  infm3  12179  prime  12649  raluz  12886  zsupss  12927  uzsupss  12930  xrsupsslem  13292  xrinfmsslem  13293  fz1sbc  13583  ssnn0fi  13956  fi1uzind  14464  brfi1indALT  14467  wrdind  14678  wrd2ind  14679  relexprelg  14991  rtrclreclem3  15013  relexpindlem  15016  relexpind  15017  rtrclind  15018  rexanre  15299  rexico  15306  reusq0  15415  limsupgle  15427  ello12  15466  ello12r  15467  ello1d  15473  elo12  15477  elo12r  15478  lo1resb  15514  o1resb  15516  rlimcn3  15540  addcn2  15544  mulcn2  15546  lo1le  15604  rpnnen2lem12  16174  sqrt2irr  16198  dfgcd2  16494  exprmfct  16647  isprm5  16650  isprm7  16651  prmdvdsexpr  16660  prmpwdvds  16843  vdwmc2  16918  ramtlecl  16939  ramub  16952  rami  16954  ramcl  16968  firest  17384  mreexexd  17598  acsfn  17609  prslem  18257  ispos  18273  posi  18276  isposd  18282  pospropd  18286  lubeldm  18312  lubval  18315  glbeldm  18325  glbval  18328  joinval2lem  18339  meetval2lem  18353  odlem1  19446  mndodcongi  19454  gexlem1  19490  sylow1lem3  19511  efgredlemb  19657  efgred  19659  frgpnabllem1  19784  acsfn1p  20560  isrrg  21106  isdomn4  21120  xrsdsreclb  21194  islindf4  21614  mplsubglem  21779  mpllsslem  21780  ltbval  21819  opsrval  21822  mdetunilem1  22336  mdetunilem3  22338  mdetunilem4  22339  mdetunilem9  22344  chpscmat  22566  istopg  22619  isclo2  22814  neiptoptop  22857  neiptopnei  22858  lmbr  22984  ist0  23046  ist1-2  23073  t1sep2  23095  cmpfi  23134  2ndcdisj  23182  1stccn  23189  iskgen3  23275  ptpjopn  23338  hausdiag  23371  xkopt  23381  ist0-4  23455  isr0  23463  r0sep  23474  fbfinnfr  23567  fmfnfmlem2  23681  fmfnfmlem4  23683  fmfnfm  23684  cnflf  23728  cnfcf  23768  tmdgsum2  23822  tsmsf1o  23871  tsmsxplem1  23879  ustssel  23932  ustincl  23934  ustdiag  23935  ustinvel  23936  ustexhalf  23937  ust0  23946  ustuqtop4  23971  utopsnneiplem  23974  isucn2  24006  iducn  24010  metcnp  24272  txmetcnp  24278  metucn  24302  ngptgp  24367  nlmvscnlem1  24425  xrge0tsms  24572  xmetdcn2  24575  addcnlem  24602  ipcnlem1  24995  caucfil  25033  metcld  25056  metcld2  25057  ellimc2  25628  dvne0  25762  mdegleb  25816  mdegle0  25829  ply1divex  25888  fta1g  25919  dgrco  26023  plydivex  26044  fta1  26055  vieta1  26059  cxpcn3lem  26489  rlimcnp  26704  dvdsmulf1o  26932  ppiublem1  26939  dchrinv  26998  lgseisenlem2  27113  2sqlem6  27160  2sqlem8  27163  2sqlem10  27165  nocvxminlem  27513  addsprop  27696  sleadd1  27709  negsprop  27746  mulsprop  27823  istrkgc  27970  istrkgb  27971  axtgcgrid  27979  axtg5seg  27981  axtgpasch  27983  axtgeucl  27988  tgcgr4  28047  axlowdimlem15  28479  usgr2wlkneq  29278  usgr2pthlem  29285  friendshipgt3  29916  isnvlem  30128  vacn  30212  smcnlem  30215  norm3lemt  30670  isch2  30741  chlimi  30752  omlsii  30921  eigorth  31356  stcltr1i  31792  elat2  31858  funcnv5mpt  32158  xrge0infss  32238  wrdt2ind  32382  resspos  32401  xrge0tsmsd  32477  domnlcan  32644  islinds5  32752  islbs5  32768  prmidlval  32827  ist0cld  33109  qqhucn  33268  esum2d  33387  eulerpartlemgvv  33671  sgn3da  33836  sgnnbi  33840  sgnpbi  33841  tgoldbachgt  33971  axtgupdim2ALTV  33976  bnj1145  34300  bnj1171  34307  bnj1172  34308  isacycgr1  34433  acycgrcycl  34434  erdszelem8  34485  satfrnmapom  34657  mclsval  34850  mclsax  34856  mclsppslem  34870  climuzcnv  34952  elintfv  35038  ifscgr  35318  idinside  35358  brsegle  35382  trer  35506  filnetlem4  35571  bj-ssblem1  35836  bj-ssblem2  35837  bj-ax12  35839  bj-19.21t0  36013  mobidvALT  36041  currysetlem  36131  currysetlem1  36133  wl-sbrimt  36720  fin2so  36780  ptrecube  36793  poimirlem26  36819  poimirlem27  36820  heicant  36828  mbfresfi  36839  itg2addnc  36847  filbcmb  36913  sdclem2  36915  fdc  36918  fdc1  36919  rngoidmlem  37109  divrngidl  37201  pridlval  37206  smprngopr  37225  inecmo  37529  elcnvrefrels3  37710  disjlem18  37975  ax12inda  38123  ax12v2-o  38124  isat3  38482  iscvlat2N  38499  psubspset  38920  ldilfset  39284  ldilset  39285  dilfsetN  39328  dilsetN  39329  cdlemefrs29bpre0  39572  cdlemefrs29clN  39575  cdlemefrs32fva  39576  cdlemn11pre  40386  dihord2pre  40401  lpolsetN  40658  sticksstones11  41280  sticksstones12a  41281  fsuppind  41466  aomclem8  42107  hbtlem5  42174  unielss  42271  ifpbi1  42532  ifpbi12  42543  ifpbi13  42544  ntrneik2  43147  ntrneikb  43149  gneispacess2  43201  2sbc6g  43478  sbiota1  43497  uzwo4  44043  fsumiunss  44591  limsupre  44657  limsupref  44701  limsupbnd1f  44702  limsupmnf  44737  limsupre2  44741  limsupmnfuzlem  44742  limsupre2mpt  44746  limsupre3  44749  limsupre3mpt  44750  ioodvbdlimc1lem2  44948  ioodvbdlimc2lem  44950  dvmptfprodlem  44960  wallispilem3  45083  fourierdlem48  45170  sge0f1o  45398  sge0iunmptlemre  45431  sge0iunmpt  45434  vonioo  45698  vonicc  45701  fcoresf1  46079  2reu8i  46121  2reuimp0  46122  2reuimp  46123  sprsymrelfolem2  46461  paireqne  46479  nfermltlrev  46712  bgoldbachlt  46781  tgoldbachlt  46784  ply1mulgsumlem1  47156  ply1mulgsumlem2  47157  elbigo2  47327  elbigo2r  47328  logic1  47565  postcposALT  47790  postc  47791  setrecseq  47819  setrec1lem1  47821  aacllem  47937