Theorem imbi2d 340

Description: Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.)

Hypothesis

Ref	Expression
imbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
imbi2d	⊢ (𝜑 → ((𝜃 → 𝜓) ↔ (𝜃 → 𝜒)))

Proof of Theorem imbi2d

Step	Hyp	Ref	Expression
1		imbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒)))
3	2	pm5.74d 273	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  imbi2  348  pm5.42  543  orbi2d  915  19.23t  2215  axc14  2465  mojust  2536  mof  2560  eu6lem  2570  2gencl  3480  3gencl  3481  vtocl2gf  3524  vtocl3gf  3525  vtocl2g  3526  vtocl3g  3527  vtocl2ga  3530  vtocl2gaf  3531  vtocl3gaf  3533  vtocl3ga  3535  vtocl4g  3537  vtocl4ga  3538  eqeu  3661  mo2icl  3669  euind  3679  reu7  3687  reuind  3708  sbctt  3807  sbccomlem  3816  reu8nf  3824  sbcnestgfw  4370  sbcnestgf  4375  r19.36zv  4462  dedth2h  4536  dedth3h  4537  dedth4h  4538  reusngf  4628  reuprg0  4656  preq12bg  4806  elint  4905  elintrabg  4913  intab  4930  axrep1  5222  axreplem  5223  axrep2  5224  axrep6g  5232  bm1.3iiOLD  5244  reusv3  5347  swopolem  5539  solin  5556  freq1  5588  frminex  5600  vtoclr  5684  2optocl  5717  3optocl  5718  raliunxp  5785  resieq  5946  iss  5991  cnveqb  6151  reu3op  6247  reuop  6248  dfpo2  6251  preddowncl  6287  fnbrfvb  6881  fvelimab  6903  fvmptss  6950  fmptco  7071  fprg  7097  fnressn  7100  fressnfv  7102  isoselem  7284  ovg  7520  caovcan  7559  caovordig  7560  caovord  7566  tfisi  7798  tfindsg  7800  tfinds2  7803  tfinds3  7804  dfom2  7807  elom  7808  findsg  7836  finds2  7837  resf1extb  7873  f1o2ndf1  8061  poxp  8067  fnse  8072  xpord3inddlem  8093  soseq  8098  fpr3g  8224  frrlem12  8236  fpr2a  8241  wfr3g  8258  smoeq  8279  smores  8281  smogt  8296  tfrlem1  8304  tfr3  8327  oaordi  8470  oeordi  8511  oeoa  8521  oeoe  8523  nnacl  8535  nnmcl  8536  nnecl  8537  nnacom  8541  nnaordi  8542  nnawordi  8545  nnaass  8546  nndi  8547  nnmass  8548  nnmsucr  8549  nnmcom  8550  nnmordi  8555  naddssim  8609  naddoa  8626  2ecoptocl  8741  3ecoptocl  8742  undifixp  8868  xpdom2g  8997  findcard2  9085  unfi  9091  ssfi  9093  fnfi  9098  fodomfi  9207  imafiOLD  9211  fodomfiOLD  9225  finsschain  9254  marypha1lem  9328  marypha1  9329  supeq1  9340  ordiso2  9412  ordtypelem7  9421  wemaplem1  9443  inf3lem2  9530  inf3lem5  9533  infdiffi  9559  cantnfval2  9570  cantnfle  9572  cantnfp1lem3  9581  oemapval  9584  cantnflem1  9590  cantnf  9594  wemapwe  9598  cnfcom  9601  cnfcom3clem  9606  ttrclss  9621  ttrclselem2  9627  tz9.1  9630  frr3g  9660  frr2  9664  r1pwALT  9750  cplem2  9794  karden  9799  updjud  9838  infxpenc2lem2  9922  fseqenlem1  9926  dfac8clem  9934  alephinit  9997  dfac4  10024  dfac5lem5  10029  dfac2a  10032  dfac2b  10033  dfacacn  10044  dfac12lem3  10048  kmlem2  10054  kmlem13  10065  nnadju  10100  ackbij1lem16  10136  sornom  10179  infpssrlem4  10208  fin23lem14  10235  fin23lem32  10246  fin23lem34  10248  fin23lem36  10250  isf32lem1  10255  isf32lem2  10256  axcc2lem  10338  axcc3  10340  axcclem  10359  zornn0g  10407  ttukeylem5  10415  ttukeylem6  10416  axrepnd  10496  axpowndlem3  10501  zfcndrep  10516  fpwwe2lem7  10539  pwfseqlem3  10562  wunr1om  10621  wunfi  10623  tskr1om  10669  ingru  10717  grudomon  10719  axgroth3  10733  axgroth4  10734  nqereu  10831  mulcanenq  10862  elnp  10889  elnpi  10890  prlem934  10935  infm3  12092  nnindd  12156  nnaddcl  12159  nnmulcl  12160  nnne0  12170  peano5uzi  12572  uzind2  12576  nn0indd  12580  zindd  12584  fzindd  12585  uzaddcl  12808  uzwo  12815  indstr  12820  zmax  12849  xmulasslem  13191  xrsupsslem  13213  xrinfmsslem  13214  xrsupss  13215  xrinfmss  13216  flval2  13725  om2uzlti  13864  uzrdgfni  13872  rabssnn0fi  13900  mptnn0fsupp  13911  seqcl2  13934  seqfveq2  13938  seqshft2  13942  monoord  13946  seqsplit  13949  seqcaopr3  13951  seqf1olem2a  13954  seqf1o  13957  seqid2  13962  seqhomo  13963  ser1const  13972  expcllem  13986  expeq0  14006  mulexp  14015  expadd  14018  expmul  14021  expmordi  14081  leexp2r  14088  leexp1a  14089  bernneq  14143  modexp  14152  facdiv  14201  faclbnd  14204  faclbnd4lem4  14210  hashgadd  14291  hashxp  14348  hashmap  14349  hashf1lem2  14370  hashf1  14371  seqcoll  14378  wrdind  14636  wrd2ind  14637  pfxccatin12lem3  14646  cshweqrep  14735  2cshwcshw  14739  relexp0g  14936  relexpsucnnr  14939  relexpsucnnl  14944  relexpcnv  14949  relexpnndm  14955  relexpaddnn  14965  rtrclreclem1  14971  dfrtrclrec2  14972  rtrclreclem2  14973  rtrclreclem4  14975  dfrtrcl2  14976  relexpind  14978  reusq0  15379  rlim  15409  rlim2  15410  rlim0  15422  rlim0lt  15423  rlimi  15427  ello12r  15431  ello1mpt  15435  ello1d  15437  elo12r  15442  lo1o1  15446  o1lo1  15451  lo1res  15473  climshft  15490  o1compt  15501  rlimo1  15531  lo1add  15541  lo1mul  15542  rlimdiv  15560  climub  15576  climserle  15577  caucvgrlem  15587  caurcvgr  15588  iseraltlem2  15597  summolem2a  15629  sumss  15638  fsum2d  15685  fsumabs  15715  fsumrlim  15725  fsumo1  15726  fsumiun  15735  binom  15744  climcndslem1  15763  climcndslem2  15764  cvgrat  15797  clim2prod  15802  prodfn0  15808  prodfrec  15809  ntrivcvgfvn0  15813  prodmolem2a  15848  fprodabs  15888  fprodn0  15893  fprod2d  15895  binomfallfac  15955  bpolycl  15966  bpolydif  15969  fprodefsum  16009  demoivreALT  16117  ruclem8  16153  ruclem9  16154  dvdsle  16228  dvdsfac  16244  divalglem7  16317  bitsinv1  16360  sadcadd  16376  sadadd2  16378  saddisjlem  16382  smuval2  16400  smupvallem  16401  smu01lem  16403  smupval  16406  smueqlem  16408  smumullem  16410  bezoutlem4  16460  dfgcd2  16464  rplpwr  16476  nn0seqcvgd  16488  seq1st  16489  alginv  16493  algcvga  16497  algfx  16498  lcmf  16551  prmind2  16603  prmdvdsexp  16633  prmfac1  16638  reumodprminv  16723  pcmpt  16811  pcfac  16818  prmpwdvds  16823  prmreclem4  16838  vdwlem10  16909  ramval  16927  ramcl  16948  cshwrepswhash1  17021  prmlem1a  17025  imasleval  17453  ismre  17500  mreexexd  17562  lubprop  18270  lublecllem  18272  glbprop  18283  joinlem  18295  meetlem  18309  poslubmo  18323  posglbmo  18324  poslubd  18325  isglbd  18423  lubun  18429  mndind  18744  frmdgsum  18778  mulgnnass  19030  mhmmulg  19036  gsumwrev  19286  gsmsymgrfix  19348  gsmsymgreq  19352  psgnunilem3  19416  sylow1lem1  19518  efginvrel2  19647  efgsrel  19654  efgredlemd  19664  efgredlem  19667  efgred  19668  efgrelexlemb  19670  gsum2dlem2  19891  gsumcom2  19895  ablfac1eulem  19994  pgpfac1lem2  19997  pgpfac1lem5  20001  pgpfac1  20002  pgpfac  20006  isomnd  20043  omndadd  20048  srgmulgass  20143  srgpcomp  20144  srgbinom  20157  isdomn2OLD  20636  isdomn3  20639  isorng  20785  lmodvsmmulgdi  20839  cnfldexp  21350  ofldchr  21522  islindf4  21784  assamulgscm  21848  mplcoe1  21983  mplcoe3  21984  mplcoe5  21986  gsummoncoe1  22243  dmatval  22427  dmatel  22428  dmatmulcl  22435  pmatcoe1fsupp  22636  decpmataa0  22703  decpmatmulsumfsupp  22708  pmatcollpw2lem  22712  pm2mpmhmlem1  22753  fiinopn  22836  mretopd  23027  neiptoptop  23066  cnpfval  23169  iscnp3  23179  tgcn  23187  lmbr  23193  lmbr2  23194  lmbrf  23195  lmss  23233  ishaus  23257  hausnei2  23288  t1sep2  23304  fiuncmp  23339  dfconn2  23354  1stcfb  23380  2ndc1stc  23386  1stcrest  23388  1stcelcls  23396  1stccn  23398  lly1stc  23431  elkgen  23471  kgencn  23491  tx1stc  23585  xkopt  23590  cnmptcom  23613  isr0  23672  r0sep  23683  ptcmpfi  23748  isfildlem  23792  rnelfm  23888  fbflim  23911  flimrest  23918  isflf  23928  flffbas  23930  lmflf  23940  fclsrest  23959  isfcf  23969  cnextfvval  24000  tmdgsum  24030  eltsms  24068  tsmsi  24069  tsmsgsum  24074  tsmssubm  24078  tsmsres  24079  tsmsf1o  24080  isust  24139  isucn  24212  isucn2  24213  ucnima  24215  imasdsf1olem  24308  metss  24443  met1stc  24456  metcnp  24476  metcnpi  24479  metcnpi2  24480  metucn  24506  xrge0tsms  24770  fsumcn  24808  elcncf  24829  cncfi  24834  rescncf  24837  cncfco  24847  caucfil  25230  equivcau  25247  caubl  25255  caublcls  25256  ovolgelb  25428  ovolunlem1a  25444  ovolicc2lem3  25467  voliunlem1  25498  voliunlem3  25500  volsuplem  25503  volsup  25504  dyadmax  25546  vitali  25561  itg2leub  25682  itgfsum  25775  dvnadd  25878  dvnres  25880  cpnord  25884  dvnfre  25903  dvmptfsum  25926  dvferm1  25936  dvferm2  25938  rolle  25941  dvlip  25945  c1lip1  25949  lhop1  25966  deg1leb  26047  ply1divex  26089  fta1g  26122  plyco  26193  dgrcolem1  26226  dgrco  26228  dvnply2  26242  plydivex  26252  aalioulem2  26288  aalioulem3  26289  aalioulem5  26291  aaliou3lem2  26298  dvntaylp  26326  taylthlem1  26328  ulmdvlem3  26358  abelthlem9  26397  cxpmul2  26645  scvxcvx  26943  jensenlem2  26945  jensen  26946  wilthlem3  27027  perfectlem2  27188  bcmono  27235  bposlem5  27246  lgsquad2lem2  27343  addsq2reu  27398  2sqreulem1  27404  2sqreunnlem1  27407  dchrisumlem1  27447  dchrisum0flb  27468  pntpbnd1  27544  pntlemf  27563  qabvle  27583  qabvexp  27584  ostthlem2  27586  ostth2lem2  27592  nosupcbv  27661  nosupno  27662  nosupdm  27663  nosupfv  27665  nosupres  27666  nosupbnd1lem1  27667  nosupbnd1lem3  27669  nosupbnd1lem5  27671  noinfcbv  27676  noinfno  27677  noinfdm  27678  noinffv  27680  noinfres  27681  noinfbnd1lem3  27684  noinfbnd1lem5  27686  eqscut2  27767  addsproplem1  27932  addsprop  27939  negsunif  28017  mulsproplem9  28083  ssltmul2  28107  precsexlem8  28172  precsexlem9  28173  precsexlem11  28175  noseqind  28242  om2noseqrdg  28254  noseqrdgfn  28256  n0addscl  28292  n0mulscl  28293  eucliddivs  28321  peano5uzs  28348  expscllem  28373  expadds  28378  expsne0  28379  expsgt0  28380  pw2cut  28400  pw2cut2  28402  tgcgr4  28529  usgr2pth  29763  wlkiswwlks2lem4  29871  wlkiswwlks2  29874  rusgrnumwwlk  29977  clwlkclwwlklem2a  29999  clwlkclwwlklem1  30000  clwlkclwwlkfo  30010  eupth2  30240  frgr3vlem1  30274  3vfriswmgrlem  30278  3vfriswmgr  30279  wlkl0  30368  numclwlk2lem2f1o  30380  isplig  30477  isnvlem  30611  nvi  30615  nmoubi  30773  nmounbi  30777  nmblolbi  30801  ipasslem1  30832  ipassi  30842  hlim2  31193  pjhth  31394  spansni  31558  elspansn2  31568  pjige0  31692  pjcjt2  31693  pjopyth  31721  elcnop  31858  elcnfn  31883  nmopub  31909  cnopc  31914  nmfnleub  31926  elnlfn  31929  cnfnc  31931  nmbdoplb  32026  nmcexi  32027  nmcoplb  32031  lnfnmul  32049  nmbdfnlb  32051  nmcfnlb  32055  pjss2coi  32165  pjssmi  32166  isst  32214  ishst  32215  stcltr1i  32275  mdbr  32295  dmdbr  32300  mddmd2  32310  mdslmd1lem3  32328  mdslmd1lem4  32329  elat2  32341  atcvat2  32390  cdj1i  32434  iuninc  32561  fmptcof2  32661  nn0min  32829  nexple  32853  wrdt2ind  32963  ismnt  32993  xrge0tsmsd  33083  gsumwun  33086  cyc3genpm  33162  isarchi2  33195  archirng  33198  archiexdiv  33200  archiabl  33208  domnprodn0  33285  islbs5  33389  unitprodclb  33398  mxidlval  33470  1arithidom  33546  1arithufdlem3  33555  crefeq  33930  esumfzf  34154  issiga  34197  isrnsiga  34198  isldsys  34241  ismeas  34284  isrnmeas  34285  measiun  34303  eulerpartlemn  34466  sseqp1  34480  rrvsum  34539  signsply0  34636  signstfvc  34659  bnj941  34856  bnj106  34952  bnj155  34963  bnj590  34994  bnj591  34995  bnj849  35009  bnj893  35012  bnj944  35022  bnj1128  35074  r1filimi  35186  r1omhfb  35195  tz9.1regs  35202  r1omhfbregs  35205  gblacfnacd  35218  subfacp1lem6  35301  erdszelem8  35314  issconn  35342  cvmliftlem7  35407  cvmliftlem10  35410  cvmlift3lem2  35436  satfsschain  35480  satfrel  35483  satfdm  35485  satfrnmapom  35486  fmlafvel  35501  satffun  35525  mrsubvrs  35638  mclsssvlem  35678  mclsval  35679  mclsax  35685  mclsind  35686  shftvalg  35848  bccolsum  35855  iprodefisumlem  35856  faclimlem1  35859  rdgprc  35908  sbequbidv  36330  cbvsbdavw  36370  fveleq  36567  unblimceq0  36623  bj-ax12  36774  bj-bm1.3ii  37181  rdgeqoa  37487  finxpreclem6  37513  domalom  37521  ralssiun  37524  wl-ax12v2cl  37623  wl-sblimt  37665  wl-sbhbt  37671  wl-2sb6d  37675  wl-mo2df  37687  wl-mo2t  37692  poimirlem2  37735  poimirlem25  37758  poimirlem28  37761  poimirlem31  37764  heicant  37768  mbfresfi  37779  itg2gt0cn  37788  sdclem2  37855  fdc  37858  seqpo  37860  incsequz  37861  mettrifi  37870  prdsbnd2  37908  heiborlem4  37927  bfplem1  37935  iscringd  38111  maxidlval  38152  igenval2  38179  iss2  38449  elrefrels3  38684  ax12eq  39113  ax12el  39114  ax12indalem  39117  ax12inda2ALT  39118  ax12inda  39120  ax12v2-o  39121  riotasvd  39128  isopos  39352  isat3  39479  ishlat1  39524  glbconN  39549  ispsubsp  39917  isldil  40282  isltrn  40291  isdilN  40326  trlval  40334  cdleme27b  40540  cdleme29b  40547  cdleme31sn1  40553  cdleme31sn1c  40560  cdleme40v  40641  cdlemk36  41085  cdlemkid5  41107  cdlemn11pre  41382  dihord2pre  41397  islpolN  41655  hdmapffval  41998  hdmapfval  41999  hdmapval2lem  42003  uzindd  42143  sticksstones1  42312  sticksstones2  42313  sticksstones3  42314  sticksstones8  42319  sticksstones10  42321  sticksstones11  42322  sticksstones12a  42323  sticksstones15  42327  indstrd  42359  unitscyglem3  42363  nnaddcom  42438  nnadddir  42440  nnmulcom  42442  eu6w  42834  ismrc  42858  incssnn0  42868  mzpexpmpt  42902  pell14qrexpclnn0  43023  monotuz  43098  rmxypos  43104  jm2.17a  43117  jm2.17b  43118  rmygeid  43121  jm2.18  43145  jm2.19lem3  43148  jm2.25  43156  jm2.15nn0  43160  jm2.16nn0  43161  wepwsolem  43199  aomclem8  43218  dfac11  43219  pwslnm  43251  lnr2i  43273  hbtlem5  43285  cnsrexpcl  43322  rngunsnply  43326  unielss  43375  onsucf1lem  43426  cantnfresb  43481  onmcl  43488  naddonnn  43552  elmapintrab  43733  elmapintab  43753  cnvcnvintabd  43757  eliunov2  43836  relexpxpnnidm  43860  relexpiidm  43861  relexpss1d  43862  iunrelexpmin1  43865  relexpmulnn  43866  iunrelexpmin2  43869  relexp0a  43873  trclimalb2  43883  clsk3nimkb  44197  ntrclsiso  44224  ntrclskb  44226  ntrneiiso  44248  ntrneix2  44250  ntrneixb  44252  gneispace2  44289  gneispacess2  44303  mnuunid  44434  dvgrat  44469  pm14.122b  44580  relpeq1  45101  relpeq3  45103  trfr  45119  pwclaxpow  45141  prclaxpr  45142  uniclaxun  45143  modelac8prim  45149  permaxpow  45166  permaxpr  45167  permaxun  45168  nregmodel  45174  fnchoice  45190  fiiuncl  45226  ssinc  45247  ssdec  45248  wessf1ornlem  45345  dmrelrnrel  45386  fperiodmullem  45467  monoordxrv  45641  fmul01  45742  fmuldfeq  45745  climsuselem1  45769  climinff  45773  ellimcabssub0  45779  limcleqr  45804  addlimc  45808  0ellimcdiv  45809  limclner  45811  limsupref  45845  limsupub  45864  limsupmnf  45881  limsupre2lem  45884  limsupre2  45885  limsupre2mpt  45890  limsupre3lem  45892  limsupre3  45893  limsupre3mpt  45894  xlimbr  45987  cnrefiisplem  45989  dvnmptdivc  46098  dvnmptconst  46101  dvnmul  46103  iblspltprt  46133  itgspltprt  46139  stoweidlem2  46162  stoweidlem3  46163  stoweidlem17  46177  stoweidlem19  46179  stoweidlem21  46181  stoweidlem26  46186  fourierdlem42  46309  issal  46474  ismea  46611  isome  46654  carageniuncllem1  46681  caratheodorylem1  46686  2reu8i  47275  2reuimp0  47276  funressndmafv2rn  47385  2ffzoeq  47489  smonoord  47533  fargshiftf1  47603  ichnfimlem  47625  paireqne  47673  reupr  47684  reuopreuprim  47688  perfectALTVlem2  47884  grimcnv  48050  pgnbgreunbgrlem1  48275  pgnbgreunbgrlem4  48281  pgnbgreunbgr  48287  lmodvsmdi  48541  dmatALTval  48562  dmatALTbasel  48564  snlindsntor  48633  ldepsnlinc  48670  elbigo2r  48715  elbigolo1  48719  itcovalt2  48839  mof0  48999  isnrm4  49092  iscnrm3r  49109  iscnrm4  49115  lubsscl  49121  glbsscl  49122  ipolubdm  49148  ipoglbdm  49151  setrecseq  49846  setrec2fun  49853  setrec2lem2  49855