Theorem imbi1d 344

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 251	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	imim1d 83	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) → (𝜒 → 𝜃)))
4	1	biimpd 232	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
5	4	imim1d 83	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))
6	3, 5	impbid 215	1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  imbi12d  347  imbi1  350  imim21b  400  pm5.33  849  con3ALT  1101  norasslem3  1565  sbjust  2097  sbequ  2119  sb6  2121  19.21t  2242  sb4b  2504  drsb1  2524  cbvralsvw  3313  sbralie  3338  raleqf  3341  ralcom2  3362  rmoeq1  3396  rspceaimv  3582  ralxpxfr2d  3599  alexeqg  3604  elab6g  3622  mo2icl  3671  sbc19.21g  3809  csbiebg  3879  ralss  3982  r19.37zv  4462  reuprg0  4659  unissb  4900  intmin4  4936  dftr2c  5214  ssexgOLD  5284  pocl  5566  vtoclr  5713  frsn  5739  cotrg  6106  dffun2  6551  fun11  6617  funimass4  6952  dff13  7260  f1mpt  7267  isopolem  7355  fnssintima  7374  oprabidw  7453  oprabid  7454  caovcan  7627  imaeqalov  7662  caoftrn  7736  ordunisuc2  7857  tfisi  7872  tfinds  7873  tfindsg  7874  tfindsg2  7875  dfom2  7881  findsg  7911  frxp  8142  xpord2indlem  8168  xpord3inddlem  8175  poseq  8179  frrlem12  8320  dfsmo2  8360  qliftfun  8828  ecoptocl  8833  ecopovtrn  8846  dom2lem  9024  findcard  9184  findcard2  9185  ssfi  9193  findcard3  9279  fiint  9323  supmo  9449  eqsup  9453  suplub  9457  supisoex  9472  infmo  9494  wemaplem1  9545  wemaplem2  9546  wemapsolem  9549  oemapvali  9690  cantnf  9699  wemapwe  9703  ttrclss  9726  kardenOLD  9965  setrec1lem1  9971  aceq1  10201  zorn2lem1  10579  axrepndlem2  10683  axregndlem2  10693  gruurn  10888  indpi  10997  nqereu  11019  prcdnq  11083  supexpr  11144  ltsosr  11184  supsrlem  11201  supsr  11202  axpre-lttrn  11256  axpre-sup  11259  prodgt0  12169  infm3  12281  prime  12785  raluz  13028  zsupss  13069  uzsupss  13072  xrsupsslem  13442  xrinfmsslem  13443  fz1sbc  13739  ssnn0fi  14133  fi1uzind  14657  brfi1indALT  14660  wrdind  14877  wrd2ind  14878  relexprelg  15198  rtrclreclem3  15220  relexpindlem  15223  relexpind  15224  rtrclind  15225  sgn3da  15261  sgnnbi  15264  sgnpbi  15265  rexanre  15521  rexico  15528  reusq0  15639  limsupgle  15651  ello12  15690  ello12r  15691  ello1d  15697  elo12  15701  elo12r  15702  lo1resb  15738  o1resb  15740  rlimcn3  15764  addcn2  15768  mulcn2  15770  lo1le  15826  rpnnen2lem12  16400  sqrt2irr  16424  dfgcd2  16726  exprmfct  16887  isprm5  16890  isprm7  16891  prmdvdsexpr  16900  prmpwdvds  17089  vdwmc2  17164  ramtlecl  17185  ramub  17198  rami  17200  ramcl  17214  firest  17610  mreexexd  17829  acsfn  17840  prslem  18478  ispos  18495  posi  18498  isposd  18503  pospropd  18506  lubeldm  18532  lubval  18535  glbeldm  18545  glbval  18548  joinval2lem  18559  meetval2lem  18573  resspos  18610  odlem1  19756  mndodcongi  19764  gexlem1  19800  sylow1lem3  19821  efgredlemb  19967  efgred  19969  frgpnabllem1  20094  isrrg  20957  isdomn4  20974  domnlcanb  20978  domnrcanb  20980  acsfn1p  21063  prmidlval  21625  xrsdsreclb  21727  islindf4  22151  mplsubglem  22313  mpllsslem  22314  ltbval  22359  opsrval  22362  psdmul  22494  mdetunilem1  22934  mdetunilem3  22936  mdetunilem4  22937  mdetunilem9  22942  chpscmat  23167  istopg  23220  isclo2  23413  neiptoptop  23456  neiptopnei  23457  lmbr  23583  ist0  23645  ist1-2  23672  t1sep2  23694  cmpfi  23733  2ndcdisj  23782  1stccn  23789  iskgen3  23875  ptpjopn  23938  hausdiag  23971  xkopt  23981  ist0-4  24055  isr0  24063  r0sep  24074  fbfinnfr  24167  fmfnfmlem2  24281  fmfnfmlem4  24283  fmfnfm  24284  cnflf  24328  cnfcf  24368  tmdgsum2  24422  tsmsf1o  24471  tsmsxplem1  24479  ustssel  24532  ustincl  24534  ustdiag  24535  ustinvel  24536  ustexhalf  24537  ust0  24546  ustuqtop4  24570  utopsnneiplem  24573  isucn2  24604  iducn  24608  metcnp  24867  txmetcnp  24873  metucn  24897  ngptgp  24962  nlmvscnlem1  25012  xrge0tsms  25161  xmetdcn2  25164  addcnlem  25191  ipcnlem1  25573  caucfil  25611  metcld  25634  metcld2  25635  ellimc2  26204  dvne0  26338  mdegleb  26389  mdegle0  26402  ply1divex  26462  fta1g  26495  dgrco  26601  plydivex  26625  fta1  26636  vieta1  26642  cxpcn3lem  27082  rlimcnp  27300  mpodvdsmulf1o  27528  dvdsmulf1o  27530  ppiublem1  27536  dchrinv  27595  lgseisenlem2  27710  2sqlem6  27757  2sqlem8  27760  2sqlem10  27762  nocvxminlem  28147  addsprop  28369  leadds1  28382  negsprop  28428  mulsprop  28523  bdayons  28669  onsfi  28749  expsne0  28829  istrkgc  28923  istrkgb  28924  axtgcgrid  28932  axtg5seg  28934  axtgpasch  28936  axtgeucl  28941  tgcgr4  29001  axlowdimlem15  29541  usgr2wlkneq  30349  usgr2pthlem  30356  isacycgr1  30759  acycgrcycl  30760  friendshipgt3  31006  isnvlem  31219  vacn  31303  smcnlem  31306  norm3lemt  31761  isch2  31832  chlimi  31843  omlsii  32012  eigorth  32447  stcltr1i  32883  elat2  32949  funcnv5mpt  33310  xrge0infss  33400  wrdt2ind  33564  xrge0tsmsd  33682  elrgspnlem4  33854  islinds5  33971  islbs5  33983  rprmdvdspow  34113  1arithufdlem3  34126  evl1deg1  34156  evl1deg2  34157  evl1deg3  34158  ply1dg1rt  34160  ist0cld  34513  qqhucn  34672  esum2d  34773  eulerpartlemgvv  35056  tgoldbachgt  35340  axtgupdim2ALTV  35345  bnj1145  35671  bnj1171  35678  bnj1172  35679  tz9.1regs  35860  srepdf  36008  erdszelem8  36051  satfrnmapom  36223  mclsval  36416  mclsax  36422  mclsppslem  36436  climuzcnv  36524  elintfv  36624  ifscgr  36903  idinside  36943  brsegle  36967  ixpeq12dv  37099  trer  37198  filnetlem4  37263  axtcond  37360  axuntco  37361  dfttc4lem1  37410  mh-setindnd  37419  mh-unprimbi  37426  mh-regprimbi  37427  mh-infprim2bi  37429  bj-ssblem1  37647  bj-ssblem2  37648  bj-ax12  37650  bj-19.21t0  37836  mobidvALT  37863  currysetlem  37952  currysetlem1  37954  wl-ax12v2cl  38536  wl-sbrimt  38586  fin2so  38637  ptrecube  38645  poimirlem26  38671  poimirlem27  38672  heicant  38680  mbfresfi  38691  itg2addnc  38699  findcard4  38739  filbcmb  38781  sdclem2  38783  fdc  38786  fdc1  38787  rngoidmlem  38977  divrngidl  39069  pridlval  39074  smprngopr  39093  inecmo  39394  elcnvrefrels3  39654  eldisjdmqsim2  39855  qmapeldisjsim  39899  rnqmapeleldisjsim  39901  disjlem18  39942  ax12inda  40112  ax12v2-o  40113  isat3  40471  iscvlat2N  40488  psubspset  40908  ldilfset  41272  ldilset  41273  dilfsetN  41316  dilsetN  41317  cdlemefrs29bpre0  41560  cdlemefrs29clN  41563  cdlemefrs32fva  41564  cdlemn11pre  42374  dihord2pre  42389  lpolsetN  42646  isprimroot  43250  primrootsunit1  43254  primrootscoprbij  43259  aks6d1c1  43273  hashscontpow  43279  sticksstones11  43313  sticksstones12a  43314  aks6d1c6lem3  43329  fimgmcyc  43705  fsuppind  43725  aomclem8  44170  hbtlem5  44237  unielss  44327  ifpbi1  44585  ifpbi12  44596  ifpbi13  44597  ntrneik2  45199  ntrneikb  45201  gneispacess2  45253  2sbc6g  45506  sbiota1  45525  relpeq2  46042  nregmodel  46114  uzwo4  46177  iineq12dv  46228  fsumiunss  46694  limsupre  46758  limsupref  46802  limsupbnd1f  46803  limsupmnf  46838  limsupre2  46842  limsupmnfuzlem  46843  limsupre2mpt  46847  limsupre3  46850  limsupre3mpt  46851  ioodvbdlimc1lem2  47049  ioodvbdlimc2lem  47051  dvmptfprodlem  47061  wallispilem3  47184  fourierdlem48  47271  sge0f1o  47499  sge0iunmptlemre  47532  sge0iunmpt  47535  vonioo  47799  vonicc  47802  fcoresf1  48246  2reu8i  48290  2reuimp0  48291  2reuimp  48292  sprsymrelfolem2  48682  paireqne  48700  nfermltlrev  48949  bgoldbachlt  49018  tgoldbachlt  49021  gpgedgiov  49270  gpgedg2ov  49271  gpgedg2iv  49272  pgnbgreunbgrlem1  49318  pgnbgreunbgrlem3  49323  pgnbgreunbgrlem4  49324  pgnbgreunbgrlem6  49329  pgnbgreunbgr  49330  smprngprmrng  49543  ply1mulgsumlem1  49605  ply1mulgsumlem2  49606  elbigo2  49771  elbigo2r  49772  imbi12d2  50008  postcposALT  50813  postc  50814  setrecseq  50970  aacllem  51121