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  834  con3ALT  1082  norasslem3  1529  sbjust  2058  sbequ  2078  sb6  2080  19.21t  2194  sb4b  2468  drsb1  2488  raleqf  3336  ralcom2  3360  rmoeq1  3400  rspceaimv  3612  ralxpxfr2d  3629  alexeqg  3634  elab6g  3654  mo2icl  3706  sbc19.21g  3851  csbiebg  3922  ralss  4051  r19.37zv  4503  reuprg0  4708  unissb  4943  intmin4  4981  dftr2c  5269  ssexg  5324  pocl  5597  poclOLD  5598  vtoclr  5741  frsn  5765  cotrg  6114  dffun2  6559  fun11  6628  funimass4  6962  dff13  7265  f1mpt  7271  isopolem  7352  fnssintima  7369  oprabidw  7450  oprabid  7451  caovcan  7625  imaeqalov  7660  caoftrn  7724  ordunisuc2  7849  tfisi  7864  tfinds  7865  tfindsg  7866  tfindsg2  7867  dfom2  7873  findsg  7905  frxp  8131  xpord2indlem  8152  xpord3inddlem  8159  poseq  8163  frrlem12  8303  dfsmo2  8368  qliftfun  8821  ecoptocl  8826  ecopovtrn  8839  dom2lem  9013  findcard  9188  findcard2  9189  ssfi  9198  findcard2OLD  9309  findcard3  9310  findcard3OLD  9311  fiint  9350  supmo  9477  eqsup  9481  suplub  9485  supisoex  9499  infmo  9520  wemaplem1  9571  wemaplem2  9572  wemapsolem  9575  oemapvali  9709  cantnf  9718  wemapwe  9722  ttrclss  9745  karden  9920  aceq1  10142  zorn2lem1  10521  axrepndlem2  10618  axregndlem2  10628  pwfseqlem4  10687  gruurn  10823  indpi  10932  nqereu  10954  prcdnq  11018  supexpr  11079  ltsosr  11119  supsrlem  11136  supsr  11137  axpre-lttrn  11191  axpre-sup  11194  prodgt0  12094  infm3  12206  prime  12676  raluz  12913  zsupss  12954  uzsupss  12957  xrsupsslem  13321  xrinfmsslem  13322  fz1sbc  13612  ssnn0fi  13986  fi1uzind  14494  brfi1indALT  14497  wrdind  14708  wrd2ind  14709  relexprelg  15021  rtrclreclem3  15043  relexpindlem  15046  relexpind  15047  rtrclind  15048  rexanre  15329  rexico  15336  reusq0  15445  limsupgle  15457  ello12  15496  ello12r  15497  ello1d  15503  elo12  15507  elo12r  15508  lo1resb  15544  o1resb  15546  rlimcn3  15570  addcn2  15574  mulcn2  15576  lo1le  15634  rpnnen2lem12  16205  sqrt2irr  16229  dfgcd2  16525  exprmfct  16678  isprm5  16681  isprm7  16682  prmdvdsexpr  16691  prmpwdvds  16876  vdwmc2  16951  ramtlecl  16972  ramub  16985  rami  16987  ramcl  17001  firest  17417  mreexexd  17631  acsfn  17642  prslem  18293  ispos  18309  posi  18312  isposd  18318  pospropd  18322  lubeldm  18348  lubval  18351  glbeldm  18361  glbval  18364  joinval2lem  18375  meetval2lem  18389  odlem1  19502  mndodcongi  19510  gexlem1  19546  sylow1lem3  19567  efgredlemb  19713  efgred  19715  frgpnabllem1  19840  acsfn1p  20699  isrrg  21252  isdomn4  21267  xrsdsreclb  21363  islindf4  21789  mplsubglem  21961  mpllsslem  21962  ltbval  22003  opsrval  22006  psdmul  22113  mdetunilem1  22558  mdetunilem3  22560  mdetunilem4  22561  mdetunilem9  22566  chpscmat  22788  istopg  22841  isclo2  23036  neiptoptop  23079  neiptopnei  23080  lmbr  23206  ist0  23268  ist1-2  23295  t1sep2  23317  cmpfi  23356  2ndcdisj  23404  1stccn  23411  iskgen3  23497  ptpjopn  23560  hausdiag  23593  xkopt  23603  ist0-4  23677  isr0  23685  r0sep  23696  fbfinnfr  23789  fmfnfmlem2  23903  fmfnfmlem4  23905  fmfnfm  23906  cnflf  23950  cnfcf  23990  tmdgsum2  24044  tsmsf1o  24093  tsmsxplem1  24101  ustssel  24154  ustincl  24156  ustdiag  24157  ustinvel  24158  ustexhalf  24159  ust0  24168  ustuqtop4  24193  utopsnneiplem  24196  isucn2  24228  iducn  24232  metcnp  24494  txmetcnp  24500  metucn  24524  ngptgp  24589  nlmvscnlem1  24647  xrge0tsms  24794  xmetdcn2  24797  addcnlem  24824  ipcnlem1  25217  caucfil  25255  metcld  25278  metcld2  25279  ellimc2  25850  dvne0  25988  mdegleb  26044  mdegle0  26057  ply1divex  26117  fta1g  26149  dgrco  26255  plydivex  26277  fta1  26288  vieta1  26292  cxpcn3lem  26727  rlimcnp  26942  mpodvdsmulf1o  27171  dvdsmulf1o  27173  ppiublem1  27180  dchrinv  27239  lgseisenlem2  27354  2sqlem6  27401  2sqlem8  27404  2sqlem10  27406  nocvxminlem  27756  addsprop  27939  sleadd1  27952  negsprop  27993  mulsprop  28080  istrkgc  28330  istrkgb  28331  axtgcgrid  28339  axtg5seg  28341  axtgpasch  28343  axtgeucl  28348  tgcgr4  28407  axlowdimlem15  28839  usgr2wlkneq  29642  usgr2pthlem  29649  friendshipgt3  30280  isnvlem  30492  vacn  30576  smcnlem  30579  norm3lemt  31034  isch2  31105  chlimi  31116  omlsii  31285  eigorth  31720  stcltr1i  32156  elat2  32222  funcnv5mpt  32535  xrge0infss  32612  wrdt2ind  32763  resspos  32782  xrge0tsmsd  32861  domnlcan  33066  islinds5  33178  islbs5  33192  prmidlval  33249  rprmdvdspow  33345  1arithufdlem3  33361  evl1deg1  33387  ply1dg1rt  33388  ist0cld  33565  qqhucn  33724  esum2d  33843  eulerpartlemgvv  34127  sgn3da  34292  sgnnbi  34296  sgnpbi  34297  tgoldbachgt  34426  axtgupdim2ALTV  34431  bnj1145  34755  bnj1171  34762  bnj1172  34763  isacycgr1  34887  acycgrcycl  34888  erdszelem8  34939  satfrnmapom  35111  mclsval  35304  mclsax  35310  mclsppslem  35324  climuzcnv  35406  elintfv  35491  ifscgr  35771  idinside  35811  brsegle  35835  trer  35931  filnetlem4  35996  bj-ssblem1  36261  bj-ssblem2  36262  bj-ax12  36264  bj-19.21t0  36438  mobidvALT  36465  currysetlem  36555  currysetlem1  36557  wl-sbrimt  37145  fin2so  37211  ptrecube  37224  poimirlem26  37250  poimirlem27  37251  heicant  37259  mbfresfi  37270  itg2addnc  37278  filbcmb  37344  sdclem2  37346  fdc  37349  fdc1  37350  rngoidmlem  37540  divrngidl  37632  pridlval  37637  smprngopr  37656  inecmo  37957  elcnvrefrels3  38137  disjlem18  38402  ax12inda  38550  ax12v2-o  38551  isat3  38909  iscvlat2N  38926  psubspset  39347  ldilfset  39711  ldilset  39712  dilfsetN  39755  dilsetN  39756  cdlemefrs29bpre0  39999  cdlemefrs29clN  40002  cdlemefrs32fva  40003  cdlemn11pre  40813  dihord2pre  40828  lpolsetN  41085  isprimroot  41696  primrootsunit1  41699  primrootscoprbij  41705  aks6d1c1  41719  hashscontpow  41725  sticksstones11  41759  sticksstones12a  41760  aks6d1c6lem3  41775  fsuppind  41958  aomclem8  42627  hbtlem5  42694  unielss  42788  ifpbi1  43049  ifpbi12  43060  ifpbi13  43061  ntrneik2  43664  ntrneikb  43666  gneispacess2  43718  2sbc6g  43994  sbiota1  44013  uzwo4  44559  fsumiunss  45101  limsupre  45167  limsupref  45211  limsupbnd1f  45212  limsupmnf  45247  limsupre2  45251  limsupmnfuzlem  45252  limsupre2mpt  45256  limsupre3  45259  limsupre3mpt  45260  ioodvbdlimc1lem2  45458  ioodvbdlimc2lem  45460  dvmptfprodlem  45470  wallispilem3  45593  fourierdlem48  45680  sge0f1o  45908  sge0iunmptlemre  45941  sge0iunmpt  45944  vonioo  46208  vonicc  46211  fcoresf1  46589  2reu8i  46631  2reuimp0  46632  2reuimp  46633  sprsymrelfolem2  46970  paireqne  46988  nfermltlrev  47221  bgoldbachlt  47290  tgoldbachlt  47293  ply1mulgsumlem1  47640  ply1mulgsumlem2  47641  elbigo2  47811  elbigo2r  47812  logic1  48049  postcposALT  48273  postc  48274  setrecseq  48302  setrec1lem1  48304  aacllem  48420