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  836  con3ALT  1085  norasslem3  1538  sbjust  2067  sbequ  2089  sb6  2091  19.21t  2214  sb4b  2480  drsb1  2500  cbvralsvw  3289  sbralie  3316  raleqf  3319  ralcom2  3340  rmoeq1  3374  rspceaimv  3571  ralxpxfr2d  3589  alexeqg  3594  elab6g  3612  mo2icl  3661  sbc19.21g  3801  csbiebg  3870  ralss  3997  ralssOLD  3999  r19.37zv  4448  reuprg0  4647  unissb  4884  intmin4  4920  dftr2c  5196  ssexg  5260  pocl  5540  vtoclr  5687  frsn  5712  cotrg  6068  dffun2  6502  fun11  6566  funimass4  6898  dff13  7202  f1mpt  7209  isopolem  7293  fnssintima  7310  oprabidw  7391  oprabid  7392  caovcan  7564  imaeqalov  7599  caoftrn  7665  ordunisuc2  7788  tfisi  7803  tfinds  7804  tfindsg  7805  tfindsg2  7806  dfom2  7812  findsg  7841  frxp  8069  xpord2indlem  8090  xpord3inddlem  8097  poseq  8101  frrlem12  8240  dfsmo2  8280  qliftfun  8742  ecoptocl  8747  ecopovtrn  8760  dom2lem  8932  findcard  9091  findcard2  9092  ssfi  9100  findcard3  9186  fiint  9230  supmo  9358  eqsup  9362  suplub  9366  supisoex  9381  infmo  9403  wemaplem1  9454  wemaplem2  9455  wemapsolem  9458  oemapvali  9596  cantnf  9605  wemapwe  9609  ttrclss  9632  karden  9810  aceq1  10030  zorn2lem1  10409  axrepndlem2  10507  axregndlem2  10517  gruurn  10712  indpi  10821  nqereu  10843  prcdnq  10907  supexpr  10968  ltsosr  11008  supsrlem  11025  supsr  11026  axpre-lttrn  11080  axpre-sup  11083  prodgt0  11993  infm3  12106  prime  12601  raluz  12837  zsupss  12878  uzsupss  12881  xrsupsslem  13250  xrinfmsslem  13251  fz1sbc  13545  ssnn0fi  13938  fi1uzind  14460  brfi1indALT  14463  wrdind  14675  wrd2ind  14676  relexprelg  14991  rtrclreclem3  15013  relexpindlem  15016  relexpind  15017  rtrclind  15018  rexanre  15300  rexico  15307  reusq0  15418  limsupgle  15430  ello12  15469  ello12r  15470  ello1d  15476  elo12  15480  elo12r  15481  lo1resb  15517  o1resb  15519  rlimcn3  15543  addcn2  15547  mulcn2  15549  lo1le  15605  rpnnen2lem12  16183  sqrt2irr  16207  dfgcd2  16506  exprmfct  16665  isprm5  16668  isprm7  16669  prmdvdsexpr  16678  prmpwdvds  16866  vdwmc2  16941  ramtlecl  16962  ramub  16975  rami  16977  ramcl  16991  firest  17386  mreexexd  17605  acsfn  17616  prslem  18254  ispos  18271  posi  18274  isposd  18279  pospropd  18282  lubeldm  18308  lubval  18311  glbeldm  18321  glbval  18324  joinval2lem  18335  meetval2lem  18349  resspos  18386  odlem1  19501  mndodcongi  19509  gexlem1  19545  sylow1lem3  19566  efgredlemb  19712  efgred  19714  frgpnabllem1  19839  isrrg  20666  isdomn4  20684  domnlcanb  20688  domnrcanb  20690  acsfn1p  20767  xrsdsreclb  21403  islindf4  21828  mplsubglem  21987  mpllsslem  21988  ltbval  22031  opsrval  22034  psdmul  22142  mdetunilem1  22587  mdetunilem3  22589  mdetunilem4  22590  mdetunilem9  22595  chpscmat  22817  istopg  22870  isclo2  23063  neiptoptop  23106  neiptopnei  23107  lmbr  23233  ist0  23295  ist1-2  23322  t1sep2  23344  cmpfi  23383  2ndcdisj  23431  1stccn  23438  iskgen3  23524  ptpjopn  23587  hausdiag  23620  xkopt  23630  ist0-4  23704  isr0  23712  r0sep  23723  fbfinnfr  23816  fmfnfmlem2  23930  fmfnfmlem4  23932  fmfnfm  23933  cnflf  23977  cnfcf  24017  tmdgsum2  24071  tsmsf1o  24120  tsmsxplem1  24128  ustssel  24181  ustincl  24183  ustdiag  24184  ustinvel  24185  ustexhalf  24186  ust0  24195  ustuqtop4  24219  utopsnneiplem  24222  isucn2  24253  iducn  24257  metcnp  24516  txmetcnp  24522  metucn  24546  ngptgp  24611  nlmvscnlem1  24661  xrge0tsms  24810  xmetdcn2  24813  addcnlem  24840  ipcnlem1  25222  caucfil  25260  metcld  25283  metcld2  25284  ellimc2  25854  dvne0  25988  mdegleb  26039  mdegle0  26052  ply1divex  26112  fta1g  26145  dgrco  26250  plydivex  26274  fta1  26285  vieta1  26289  cxpcn3lem  26724  rlimcnp  26942  mpodvdsmulf1o  27171  dvdsmulf1o  27173  ppiublem1  27179  dchrinv  27238  lgseisenlem2  27353  2sqlem6  27400  2sqlem8  27403  2sqlem10  27405  nocvxminlem  27760  addsprop  27982  leadds1  27995  negsprop  28041  mulsprop  28136  bdayons  28282  onsfi  28362  expsne0  28442  istrkgc  28536  istrkgb  28537  axtgcgrid  28545  axtg5seg  28547  axtgpasch  28549  axtgeucl  28554  tgcgr4  28613  axlowdimlem15  29039  usgr2wlkneq  29839  usgr2pthlem  29846  friendshipgt3  30483  isnvlem  30696  vacn  30780  smcnlem  30783  norm3lemt  31238  isch2  31309  chlimi  31320  omlsii  31489  eigorth  31924  stcltr1i  32360  elat2  32426  funcnv5mpt  32755  xrge0infss  32848  sgn3da  32922  sgnnbi  32926  sgnpbi  32927  wrdt2ind  33028  xrge0tsmsd  33149  elrgspnlem4  33321  domnlcanOLD  33356  islinds5  33442  islbs5  33455  prmidlval  33512  rprmdvdspow  33608  1arithufdlem3  33621  evl1deg1  33651  evl1deg2  33652  evl1deg3  33653  ply1dg1rt  33655  ist0cld  33993  qqhucn  34152  esum2d  34253  eulerpartlemgvv  34536  tgoldbachgt  34823  axtgupdim2ALTV  34828  bnj1145  35151  bnj1171  35158  bnj1172  35159  tz9.1regs  35294  isacycgr1  35344  acycgrcycl  35345  erdszelem8  35396  satfrnmapom  35568  mclsval  35761  mclsax  35767  mclsppslem  35781  climuzcnv  35869  elintfv  35963  ifscgr  36242  idinside  36282  brsegle  36306  ixpeq12dv  36414  trer  36514  filnetlem4  36579  axtcond  36676  axuntco  36677  dfttc4lem1  36726  mh-setindnd  36735  mh-unprimbi  36742  mh-regprimbi  36743  mh-infprim2bi  36745  bj-ssblem1  36964  bj-ssblem2  36965  bj-ax12  36967  bj-19.21t0  37153  mobidvALT  37180  currysetlem  37268  currysetlem1  37270  wl-ax12v2cl  37836  wl-sbrimt  37886  fin2so  37942  ptrecube  37955  poimirlem26  37981  poimirlem27  37982  heicant  37990  mbfresfi  38001  itg2addnc  38009  filbcmb  38075  sdclem2  38077  fdc  38080  fdc1  38081  rngoidmlem  38271  divrngidl  38363  pridlval  38368  smprngopr  38387  inecmo  38690  elcnvrefrels3  38950  eldisjdmqsim2  39151  qmapeldisjsim  39195  rnqmapeleldisjsim  39197  disjlem18  39238  ax12inda  39408  ax12v2-o  39409  isat3  39767  iscvlat2N  39784  psubspset  40204  ldilfset  40568  ldilset  40569  dilfsetN  40612  dilsetN  40613  cdlemefrs29bpre0  40856  cdlemefrs29clN  40859  cdlemefrs32fva  40860  cdlemn11pre  41670  dihord2pre  41685  lpolsetN  41942  isprimroot  42546  primrootsunit1  42550  primrootscoprbij  42555  aks6d1c1  42569  hashscontpow  42575  sticksstones11  42609  sticksstones12a  42610  aks6d1c6lem3  42625  fimgmcyc  42993  fsuppind  43037  aomclem8  43507  hbtlem5  43574  unielss  43664  ifpbi1  43922  ifpbi12  43933  ifpbi13  43934  ntrneik2  44537  ntrneikb  44539  gneispacess2  44591  2sbc6g  44860  sbiota1  44879  relpeq2  45390  nregmodel  45462  uzwo4  45502  iineq12dv  45554  fsumiunss  46023  limsupre  46087  limsupref  46131  limsupbnd1f  46132  limsupmnf  46167  limsupre2  46171  limsupmnfuzlem  46172  limsupre2mpt  46176  limsupre3  46179  limsupre3mpt  46180  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvmptfprodlem  46390  wallispilem3  46513  fourierdlem48  46600  sge0f1o  46828  sge0iunmptlemre  46861  sge0iunmpt  46864  vonioo  47128  vonicc  47131  fcoresf1  47529  2reu8i  47573  2reuimp0  47574  2reuimp  47575  sprsymrelfolem2  47965  paireqne  47983  nfermltlrev  48232  bgoldbachlt  48301  tgoldbachlt  48304  gpgedgiov  48553  gpgedg2ov  48554  gpgedg2iv  48555  pgnbgreunbgrlem1  48601  pgnbgreunbgrlem3  48606  pgnbgreunbgrlem4  48607  pgnbgreunbgrlem6  48612  pgnbgreunbgr  48613  ply1mulgsumlem1  48874  ply1mulgsumlem2  48875  elbigo2  49040  elbigo2r  49041  logic1  49278  postcposALT  50055  postc  50056  setrecseq  50172  setrec1lem1  50174  aacllem  50288