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  2213  axc14  2463  mojust  2534  mof  2558  eu6lem  2568  2gencl  3479  3gencl  3480  vtocl2gf  3527  vtocl3gf  3528  vtocl2g  3529  vtocl3g  3530  vtocl2ga  3533  vtocl2gaf  3534  vtocl3gaf  3536  vtocl3ga  3538  vtocl4g  3540  vtocl4ga  3541  eqeu  3665  mo2icl  3673  euind  3683  reu7  3691  reuind  3712  sbctt  3811  sbccomlem  3820  reu8nf  3828  sbcnestgfw  4371  sbcnestgf  4376  r19.36zv  4457  dedth2h  4535  dedth3h  4536  dedth4h  4537  reusngf  4627  reuprg0  4655  preq12bg  4805  elint  4903  elintrabg  4911  intab  4928  axrep1  5218  axreplem  5219  axrep2  5220  axrep6g  5228  bm1.3iiOLD  5240  reusv3  5343  swopolem  5534  solin  5551  freq1  5583  frminex  5595  vtoclr  5679  2optocl  5712  3optocl  5713  raliunxp  5779  resieq  5939  iss  5984  cnveqb  6143  reu3op  6239  reuop  6240  dfpo2  6243  preddowncl  6279  fnbrfvb  6872  fvelimab  6894  fvmptss  6941  fmptco  7062  fprg  7088  fnressn  7091  fressnfv  7093  isoselem  7275  ovg  7511  caovcan  7550  caovordig  7551  caovord  7557  tfisi  7789  tfindsg  7791  tfinds2  7794  tfinds3  7795  dfom2  7798  elom  7799  findsg  7827  finds2  7828  resf1extb  7864  f1o2ndf1  8052  poxp  8058  fnse  8063  xpord3inddlem  8084  soseq  8089  fpr3g  8215  frrlem12  8227  fpr2a  8232  wfr3g  8249  smoeq  8270  smores  8272  smogt  8287  tfrlem1  8295  tfr3  8318  oaordi  8461  oeordi  8502  oeoa  8512  oeoe  8514  nnacl  8526  nnmcl  8527  nnecl  8528  nnacom  8532  nnaordi  8533  nnawordi  8536  nnaass  8537  nndi  8538  nnmass  8539  nnmsucr  8540  nnmcom  8541  nnmordi  8546  naddssim  8600  naddoa  8617  2ecoptocl  8732  3ecoptocl  8733  undifixp  8858  xpdom2g  8986  findcard2  9074  unfi  9080  ssfi  9082  fnfi  9087  fodomfi  9196  imafiOLD  9200  fodomfiOLD  9214  finsschain  9243  marypha1lem  9317  marypha1  9318  supeq1  9329  ordiso2  9401  ordtypelem7  9410  wemaplem1  9432  inf3lem2  9519  inf3lem5  9522  infdiffi  9548  cantnfval2  9559  cantnfle  9561  cantnfp1lem3  9570  oemapval  9573  cantnflem1  9579  cantnf  9583  wemapwe  9587  cnfcom  9590  cnfcom3clem  9595  ttrclss  9610  ttrclselem2  9616  tz9.1  9619  frr3g  9649  frr2  9653  r1pwALT  9739  cplem2  9783  karden  9788  updjud  9827  infxpenc2lem2  9911  fseqenlem1  9915  dfac8clem  9923  alephinit  9986  dfac4  10013  dfac5lem5  10018  dfac2a  10021  dfac2b  10022  dfacacn  10033  dfac12lem3  10037  kmlem2  10043  kmlem13  10054  nnadju  10089  ackbij1lem16  10125  sornom  10168  infpssrlem4  10197  fin23lem14  10224  fin23lem32  10235  fin23lem34  10237  fin23lem36  10239  isf32lem1  10244  isf32lem2  10245  axcc2lem  10327  axcc3  10329  axcclem  10348  zornn0g  10396  ttukeylem5  10404  ttukeylem6  10405  axrepnd  10485  axpowndlem3  10490  zfcndrep  10505  fpwwe2lem7  10528  pwfseqlem3  10551  wunr1om  10610  wunfi  10612  tskr1om  10658  ingru  10706  grudomon  10708  axgroth3  10722  axgroth4  10723  nqereu  10820  mulcanenq  10851  elnp  10878  elnpi  10879  prlem934  10924  infm3  12081  nnindd  12145  nnaddcl  12148  nnmulcl  12149  nnne0  12159  peano5uzi  12562  uzind2  12566  nn0indd  12570  zindd  12574  fzindd  12575  eluzaddOLD  12767  uzaddcl  12802  uzwo  12809  indstr  12814  zmax  12843  xmulasslem  13184  xrsupsslem  13206  xrinfmsslem  13207  xrsupss  13208  xrinfmss  13209  flval2  13718  om2uzlti  13857  uzrdgfni  13865  rabssnn0fi  13893  mptnn0fsupp  13904  seqcl2  13927  seqfveq2  13931  seqshft2  13935  monoord  13939  seqsplit  13942  seqcaopr3  13944  seqf1olem2a  13947  seqf1o  13950  seqid2  13955  seqhomo  13956  ser1const  13965  expcllem  13979  expeq0  13999  mulexp  14008  expadd  14011  expmul  14014  expmordi  14074  leexp2r  14081  leexp1a  14082  bernneq  14136  modexp  14145  facdiv  14194  faclbnd  14197  faclbnd4lem4  14203  hashgadd  14284  hashxp  14341  hashmap  14342  hashf1lem2  14363  hashf1  14364  seqcoll  14371  wrdind  14629  wrd2ind  14630  pfxccatin12lem3  14639  cshweqrep  14728  2cshwcshw  14732  relexp0g  14929  relexpsucnnr  14932  relexpsucnnl  14937  relexpcnv  14942  relexpnndm  14948  relexpaddnn  14958  rtrclreclem1  14964  dfrtrclrec2  14965  rtrclreclem2  14966  rtrclreclem4  14968  dfrtrcl2  14969  relexpind  14971  reusq0  15372  rlim  15402  rlim2  15403  rlim0  15415  rlim0lt  15416  rlimi  15420  ello12r  15424  ello1mpt  15428  ello1d  15430  elo12r  15435  lo1o1  15439  o1lo1  15444  lo1res  15466  climshft  15483  o1compt  15494  rlimo1  15524  lo1add  15534  lo1mul  15535  rlimdiv  15553  climub  15569  climserle  15570  caucvgrlem  15580  caurcvgr  15581  iseraltlem2  15590  summolem2a  15622  sumss  15631  fsum2d  15678  fsumabs  15708  fsumrlim  15718  fsumo1  15719  fsumiun  15728  binom  15737  climcndslem1  15756  climcndslem2  15757  cvgrat  15790  clim2prod  15795  prodfn0  15801  prodfrec  15802  ntrivcvgfvn0  15806  prodmolem2a  15841  fprodabs  15881  fprodn0  15886  fprod2d  15888  binomfallfac  15948  bpolycl  15959  bpolydif  15962  fprodefsum  16002  demoivreALT  16110  ruclem8  16146  ruclem9  16147  dvdsle  16221  dvdsfac  16237  divalglem7  16310  bitsinv1  16353  sadcadd  16369  sadadd2  16371  saddisjlem  16375  smuval2  16393  smupvallem  16394  smu01lem  16396  smupval  16399  smueqlem  16401  smumullem  16403  bezoutlem4  16453  dfgcd2  16457  rplpwr  16469  nn0seqcvgd  16481  seq1st  16482  alginv  16486  algcvga  16490  algfx  16491  lcmf  16544  prmind2  16596  prmdvdsexp  16626  prmfac1  16631  reumodprminv  16716  pcmpt  16804  pcfac  16811  prmpwdvds  16816  prmreclem4  16831  vdwlem10  16902  ramval  16920  ramcl  16941  cshwrepswhash1  17014  prmlem1a  17018  imasleval  17445  ismre  17492  mreexexd  17554  lubprop  18262  lublecllem  18264  glbprop  18275  joinlem  18287  meetlem  18301  poslubmo  18315  posglbmo  18316  poslubd  18317  isglbd  18415  lubun  18421  mndind  18736  frmdgsum  18770  mulgnnass  19022  mhmmulg  19028  gsumwrev  19279  gsmsymgrfix  19341  gsmsymgreq  19345  psgnunilem3  19409  sylow1lem1  19511  efginvrel2  19640  efgsrel  19647  efgredlemd  19657  efgredlem  19660  efgred  19661  efgrelexlemb  19663  gsum2dlem2  19884  gsumcom2  19888  ablfac1eulem  19987  pgpfac1lem2  19990  pgpfac1lem5  19994  pgpfac1  19995  pgpfac  19999  isomnd  20036  omndadd  20041  srgmulgass  20136  srgpcomp  20137  srgbinom  20150  isdomn2OLD  20628  isdomn3  20631  isorng  20777  lmodvsmmulgdi  20831  cnfldexp  21342  ofldchr  21514  islindf4  21776  assamulgscm  21839  mplcoe1  21973  mplcoe3  21974  mplcoe5  21976  gsummoncoe1  22224  dmatval  22408  dmatel  22409  dmatmulcl  22416  pmatcoe1fsupp  22617  decpmataa0  22684  decpmatmulsumfsupp  22689  pmatcollpw2lem  22693  pm2mpmhmlem1  22734  fiinopn  22817  mretopd  23008  neiptoptop  23047  cnpfval  23150  iscnp3  23160  tgcn  23168  lmbr  23174  lmbr2  23175  lmbrf  23176  lmss  23214  ishaus  23238  hausnei2  23269  t1sep2  23285  fiuncmp  23320  dfconn2  23335  1stcfb  23361  2ndc1stc  23367  1stcrest  23369  1stcelcls  23377  1stccn  23379  lly1stc  23412  elkgen  23452  kgencn  23472  tx1stc  23566  xkopt  23571  cnmptcom  23594  isr0  23653  r0sep  23664  ptcmpfi  23729  isfildlem  23773  rnelfm  23869  fbflim  23892  flimrest  23899  isflf  23909  flffbas  23911  lmflf  23921  fclsrest  23940  isfcf  23950  cnextfvval  23981  tmdgsum  24011  eltsms  24049  tsmsi  24050  tsmsgsum  24055  tsmssubm  24059  tsmsres  24060  tsmsf1o  24061  isust  24120  isucn  24193  isucn2  24194  ucnima  24196  imasdsf1olem  24289  metss  24424  met1stc  24437  metcnp  24457  metcnpi  24460  metcnpi2  24461  metucn  24487  xrge0tsms  24751  fsumcn  24789  elcncf  24810  cncfi  24815  rescncf  24818  cncfco  24828  caucfil  25211  equivcau  25228  caubl  25236  caublcls  25237  ovolgelb  25409  ovolunlem1a  25425  ovolicc2lem3  25448  voliunlem1  25479  voliunlem3  25481  volsuplem  25484  volsup  25485  dyadmax  25527  vitali  25542  itg2leub  25663  itgfsum  25756  dvnadd  25859  dvnres  25861  cpnord  25865  dvnfre  25884  dvmptfsum  25907  dvferm1  25917  dvferm2  25919  rolle  25922  dvlip  25926  c1lip1  25930  lhop1  25947  deg1leb  26028  ply1divex  26070  fta1g  26103  plyco  26174  dgrcolem1  26207  dgrco  26209  dvnply2  26223  plydivex  26233  aalioulem2  26269  aalioulem3  26270  aalioulem5  26272  aaliou3lem2  26279  dvntaylp  26307  taylthlem1  26309  ulmdvlem3  26339  abelthlem9  26378  cxpmul2  26626  scvxcvx  26924  jensenlem2  26926  jensen  26927  wilthlem3  27008  perfectlem2  27169  bcmono  27216  bposlem5  27227  lgsquad2lem2  27324  addsq2reu  27379  2sqreulem1  27385  2sqreunnlem1  27388  dchrisumlem1  27428  dchrisum0flb  27449  pntpbnd1  27525  pntlemf  27544  qabvle  27564  qabvexp  27565  ostthlem2  27567  ostth2lem2  27573  nosupcbv  27642  nosupno  27643  nosupdm  27644  nosupfv  27646  nosupres  27647  nosupbnd1lem1  27648  nosupbnd1lem3  27650  nosupbnd1lem5  27652  noinfcbv  27657  noinfno  27658  noinfdm  27659  noinffv  27661  noinfres  27662  noinfbnd1lem3  27665  noinfbnd1lem5  27667  eqscut2  27748  addsproplem1  27913  addsprop  27920  negsunif  27998  mulsproplem9  28064  ssltmul2  28088  precsexlem8  28153  precsexlem9  28154  precsexlem11  28156  noseqind  28223  om2noseqrdg  28235  noseqrdgfn  28237  n0addscl  28273  n0mulscl  28274  eucliddivs  28302  peano5uzs  28329  expscllem  28354  expadds  28359  expsne0  28360  expsgt0  28361  pw2cut  28381  pw2cut2  28383  tgcgr4  28510  usgr2pth  29743  wlkiswwlks2lem4  29851  wlkiswwlks2  29854  rusgrnumwwlk  29954  clwlkclwwlklem2a  29976  clwlkclwwlklem1  29977  clwlkclwwlkfo  29987  eupth2  30217  frgr3vlem1  30251  3vfriswmgrlem  30255  3vfriswmgr  30256  wlkl0  30345  numclwlk2lem2f1o  30357  isplig  30454  isnvlem  30588  nvi  30592  nmoubi  30750  nmounbi  30754  nmblolbi  30778  ipasslem1  30809  ipassi  30819  hlim2  31170  pjhth  31371  spansni  31535  elspansn2  31545  pjige0  31669  pjcjt2  31670  pjopyth  31698  elcnop  31835  elcnfn  31860  nmopub  31886  cnopc  31891  nmfnleub  31903  elnlfn  31906  cnfnc  31908  nmbdoplb  32003  nmcexi  32004  nmcoplb  32008  lnfnmul  32026  nmbdfnlb  32028  nmcfnlb  32032  pjss2coi  32142  pjssmi  32143  isst  32191  ishst  32192  stcltr1i  32252  mdbr  32272  dmdbr  32277  mddmd2  32287  mdslmd1lem3  32305  mdslmd1lem4  32306  elat2  32318  atcvat2  32367  cdj1i  32411  iuninc  32538  fmptcof2  32637  nn0min  32801  nexple  32825  wrdt2ind  32932  ismnt  32962  xrge0tsmsd  33040  gsumwun  33043  cyc3genpm  33119  isarchi2  33152  archirng  33155  archiexdiv  33157  archiabl  33165  domnprodn0  33240  islbs5  33343  unitprodclb  33352  mxidlval  33424  1arithidom  33500  1arithufdlem3  33509  crefeq  33856  esumfzf  34080  issiga  34123  isrnsiga  34124  isldsys  34167  ismeas  34210  isrnmeas  34211  measiun  34229  eulerpartlemn  34392  sseqp1  34406  rrvsum  34465  signsply0  34562  signstfvc  34585  bnj941  34782  bnj106  34878  bnj155  34889  bnj590  34920  bnj591  34921  bnj849  34935  bnj893  34938  bnj944  34948  bnj1128  35000  r1filimi  35112  r1omhfb  35121  tz9.1regs  35128  r1omhfbregs  35131  gblacfnacd  35144  subfacp1lem6  35227  erdszelem8  35240  issconn  35268  cvmliftlem7  35333  cvmliftlem10  35336  cvmlift3lem2  35362  satfsschain  35406  satfrel  35409  satfdm  35411  satfrnmapom  35412  fmlafvel  35427  satffun  35451  mrsubvrs  35564  mclsssvlem  35604  mclsval  35605  mclsax  35611  mclsind  35612  shftvalg  35774  bccolsum  35781  iprodefisumlem  35782  faclimlem1  35785  rdgprc  35834  sbequbidv  36254  cbvsbdavw  36294  fveleq  36491  unblimceq0  36547  bj-ax12  36697  bj-bm1.3ii  37104  rdgeqoa  37410  finxpreclem6  37436  domalom  37444  ralssiun  37447  wl-ax12v2cl  37546  wl-sblimt  37588  wl-sbhbt  37594  wl-2sb6d  37598  wl-mo2df  37610  wl-mo2t  37615  poimirlem2  37668  poimirlem25  37691  poimirlem28  37694  poimirlem31  37697  heicant  37701  mbfresfi  37712  itg2gt0cn  37721  sdclem2  37788  fdc  37791  seqpo  37793  incsequz  37794  mettrifi  37803  prdsbnd2  37841  heiborlem4  37860  bfplem1  37868  iscringd  38044  maxidlval  38085  igenval2  38112  iss2  38378  elrefrels3  38562  ax12eq  38986  ax12el  38987  ax12indalem  38990  ax12inda2ALT  38991  ax12inda  38993  ax12v2-o  38994  riotasvd  39001  isopos  39225  isat3  39352  ishlat1  39397  glbconN  39422  ispsubsp  39790  isldil  40155  isltrn  40164  isdilN  40199  trlval  40207  cdleme27b  40413  cdleme29b  40420  cdleme31sn1  40426  cdleme31sn1c  40433  cdleme40v  40514  cdlemk36  40958  cdlemkid5  40980  cdlemn11pre  41255  dihord2pre  41270  islpolN  41528  hdmapffval  41871  hdmapfval  41872  hdmapval2lem  41876  uzindd  42016  sticksstones1  42185  sticksstones2  42186  sticksstones3  42187  sticksstones8  42192  sticksstones10  42194  sticksstones11  42195  sticksstones12a  42196  sticksstones15  42200  indstrd  42232  unitscyglem3  42236  nnaddcom  42307  nnadddir  42309  nnmulcom  42311  eu6w  42715  ismrc  42740  incssnn0  42750  mzpexpmpt  42784  pell14qrexpclnn0  42905  monotuz  42980  rmxypos  42986  jm2.17a  42999  jm2.17b  43000  rmygeid  43003  jm2.18  43027  jm2.19lem3  43030  jm2.25  43038  jm2.15nn0  43042  jm2.16nn0  43043  wepwsolem  43081  aomclem8  43100  dfac11  43101  pwslnm  43133  lnr2i  43155  hbtlem5  43167  cnsrexpcl  43204  rngunsnply  43208  unielss  43257  onsucf1lem  43308  cantnfresb  43363  onmcl  43370  naddonnn  43434  elmapintrab  43615  elmapintab  43635  cnvcnvintabd  43639  eliunov2  43718  relexpxpnnidm  43742  relexpiidm  43743  relexpss1d  43744  iunrelexpmin1  43747  relexpmulnn  43748  iunrelexpmin2  43751  relexp0a  43755  trclimalb2  43765  clsk3nimkb  44079  ntrclsiso  44106  ntrclskb  44108  ntrneiiso  44130  ntrneix2  44132  ntrneixb  44134  gneispace2  44171  gneispacess2  44185  mnuunid  44316  dvgrat  44351  pm14.122b  44462  relpeq1  44983  relpeq3  44985  trfr  45001  pwclaxpow  45023  prclaxpr  45024  uniclaxun  45025  modelac8prim  45031  permaxpow  45048  permaxpr  45049  permaxun  45050  nregmodel  45056  fnchoice  45072  fiiuncl  45108  ssinc  45130  ssdec  45131  wessf1ornlem  45228  dmrelrnrel  45269  fperiodmullem  45350  monoordxrv  45525  fmul01  45626  fmuldfeq  45629  climsuselem1  45653  climinff  45657  ellimcabssub0  45663  limcleqr  45688  addlimc  45692  0ellimcdiv  45693  limclner  45695  limsupref  45729  limsupub  45748  limsupmnf  45765  limsupre2lem  45768  limsupre2  45769  limsupre2mpt  45774  limsupre3lem  45776  limsupre3  45777  limsupre3mpt  45778  xlimbr  45871  cnrefiisplem  45873  dvnmptdivc  45982  dvnmptconst  45985  dvnmul  45987  iblspltprt  46017  itgspltprt  46023  stoweidlem2  46046  stoweidlem3  46047  stoweidlem17  46061  stoweidlem19  46063  stoweidlem21  46065  stoweidlem26  46070  fourierdlem42  46193  issal  46358  ismea  46495  isome  46538  carageniuncllem1  46565  caratheodorylem1  46570  2reu8i  47150  2reuimp0  47151  funressndmafv2rn  47260  2ffzoeq  47364  smonoord  47408  fargshiftf1  47478  ichnfimlem  47500  paireqne  47548  reupr  47559  reuopreuprim  47563  perfectALTVlem2  47759  grimcnv  47925  pgnbgreunbgrlem1  48150  pgnbgreunbgrlem4  48156  pgnbgreunbgr  48162  lmodvsmdi  48416  dmatALTval  48438  dmatALTbasel  48440  snlindsntor  48509  ldepsnlinc  48546  elbigo2r  48591  elbigolo1  48595  itcovalt2  48715  mof0  48875  isnrm4  48968  iscnrm3r  48985  iscnrm4  48991  lubsscl  48997  glbsscl  48998  ipolubdm  49024  ipoglbdm  49027  setrecseq  49723  setrec2fun  49730  setrec2lem2  49732