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  2211  axc14  2468  mojust  2539  mof  2563  eu6lem  2573  2gencl  3508  3gencl  3509  vtocl2gf  3556  vtocl3gf  3557  vtocl2g  3558  vtocl3g  3559  vtocl2ga  3562  vtocl2gaf  3563  vtocl3gaf  3565  vtocl3ga  3567  vtocl4g  3569  vtocl4ga  3570  eqeu  3694  mo2icl  3702  euind  3712  reu7  3720  reuind  3741  sbctt  3840  sbccomlem  3849  reu8nf  3857  sbcnestgfw  4401  sbcnestgf  4406  r19.36zv  4487  dedth2h  4565  dedth3h  4566  dedth4h  4567  reusngf  4655  reuprg0  4683  preq12bg  4834  elint  4933  elintrabg  4942  intab  4959  axrep1  5255  axreplem  5256  axrep2  5257  axrep6g  5265  bm1.3iiOLD  5277  reusv3  5380  swopolem  5576  solin  5593  freq1  5626  frminex  5638  vtoclr  5722  2optocl  5755  3optocl  5756  raliunxp  5824  resieq  5982  iss  6027  cnveqb  6190  reu3op  6286  reuop  6287  dfpo2  6290  preddowncl  6326  funmoOLD  6557  funimaexgOLD  6629  fnbrfvb  6934  fvelimab  6956  fvmptss  7003  fmptco  7124  fprg  7150  fnressn  7153  fressnfv  7155  isoselem  7339  ovg  7577  caovcan  7616  caovordig  7617  caovord  7623  tfisi  7859  tfindsg  7861  tfinds2  7864  tfinds3  7865  dfom2  7868  elom  7869  findsg  7898  finds2  7899  resf1extb  7935  f1o2ndf1  8126  poxp  8132  fnse  8137  xpord3inddlem  8158  soseq  8163  fpr3g  8289  frrlem12  8301  fpr2a  8306  wfr3g  8326  wfrlem4OLD  8331  smoeq  8369  smores  8371  smogt  8386  tfrlem1  8395  tfr3  8418  oaordi  8563  oeordi  8604  oeoa  8614  oeoe  8616  nnacl  8628  nnmcl  8629  nnecl  8630  nnacom  8634  nnaordi  8635  nnawordi  8638  nnaass  8639  nndi  8640  nnmass  8641  nnmsucr  8642  nnmcom  8643  nnmordi  8648  naddssim  8702  naddoa  8719  2ecoptocl  8827  3ecoptocl  8828  undifixp  8953  xpdom2g  9087  findcard2  9183  unfi  9190  ssfi  9192  fnfi  9197  fodomfi  9327  imafiOLD  9331  xpfiOLD  9336  fodomfiOLD  9347  finsschain  9376  marypha1lem  9450  marypha1  9451  supeq1  9462  ordiso2  9534  ordtypelem7  9543  wemaplem1  9565  inf3lem2  9648  inf3lem5  9651  infdiffi  9677  cantnfval2  9688  cantnfle  9690  cantnfp1lem3  9699  oemapval  9702  cantnflem1  9708  cantnf  9712  wemapwe  9716  cnfcom  9719  cnfcom3clem  9724  ttrclss  9739  ttrclselem2  9745  tz9.1  9748  frr3g  9775  frr2  9779  r1pwALT  9865  cplem2  9909  karden  9914  updjud  9953  infxpenc2lem2  10039  fseqenlem1  10043  dfac8clem  10051  alephinit  10114  dfac4  10141  dfac5lem5  10146  dfac2a  10149  dfac2b  10150  dfacacn  10161  dfac12lem3  10165  kmlem2  10171  kmlem13  10182  nnadju  10217  ackbij1lem16  10253  sornom  10296  infpssrlem4  10325  fin23lem14  10352  fin23lem32  10363  fin23lem34  10365  fin23lem36  10367  isf32lem1  10372  isf32lem2  10373  axcc2lem  10455  axcc3  10457  axcclem  10476  zornn0g  10524  ttukeylem5  10532  ttukeylem6  10533  axrepnd  10613  axpowndlem3  10618  zfcndrep  10633  fpwwe2lem7  10656  pwfseqlem3  10679  wunr1om  10738  wunfi  10740  tskr1om  10786  ingru  10834  grudomon  10836  axgroth3  10850  axgroth4  10851  nqereu  10948  mulcanenq  10979  elnp  11006  elnpi  11007  prlem934  11052  infm3  12206  nnindd  12265  nnaddcl  12268  nnmulcl  12269  nnne0  12279  peano5uzi  12687  uzind2  12691  nn0indd  12695  zindd  12699  fzindd  12700  eluzaddOLD  12892  uzaddcl  12925  uzwo  12932  indstr  12937  zmax  12966  xmulasslem  13306  xrsupsslem  13328  xrinfmsslem  13329  xrsupss  13330  xrinfmss  13331  flval2  13836  om2uzlti  13973  uzrdgfni  13981  rabssnn0fi  14009  mptnn0fsupp  14020  seqcl2  14043  seqfveq2  14047  seqshft2  14051  monoord  14055  seqsplit  14058  seqcaopr3  14060  seqf1olem2a  14063  seqf1o  14066  seqid2  14071  seqhomo  14072  ser1const  14081  expcllem  14095  expeq0  14115  mulexp  14124  expadd  14127  expmul  14130  expmordi  14190  leexp2r  14197  leexp1a  14198  bernneq  14252  modexp  14261  facdiv  14310  faclbnd  14313  faclbnd4lem4  14319  hashgadd  14400  hashxp  14457  hashmap  14458  hashf1lem2  14479  hashf1  14480  seqcoll  14487  wrdind  14745  wrd2ind  14746  pfxccatin12lem3  14755  cshweqrep  14844  2cshwcshw  14849  relexp0g  15046  relexpsucnnr  15049  relexpsucnnl  15054  relexpcnv  15059  relexpnndm  15065  relexpaddnn  15075  rtrclreclem1  15081  dfrtrclrec2  15082  rtrclreclem2  15083  rtrclreclem4  15085  dfrtrcl2  15086  relexpind  15088  reusq0  15486  rlim  15516  rlim2  15517  rlim0  15529  rlim0lt  15530  rlimi  15534  ello12r  15538  ello1mpt  15542  ello1d  15544  elo12r  15549  lo1o1  15553  o1lo1  15558  lo1res  15580  climshft  15597  o1compt  15608  rlimo1  15638  lo1add  15648  lo1mul  15649  rlimdiv  15667  climub  15683  climserle  15684  caucvgrlem  15694  caurcvgr  15695  iseraltlem2  15704  summolem2a  15736  sumss  15745  fsum2d  15792  fsumabs  15822  fsumrlim  15832  fsumo1  15833  fsumiun  15842  binom  15851  climcndslem1  15870  climcndslem2  15871  cvgrat  15904  clim2prod  15909  prodfn0  15915  prodfrec  15916  ntrivcvgfvn0  15920  prodmolem2a  15955  fprodabs  15995  fprodn0  16000  fprod2d  16002  binomfallfac  16062  bpolycl  16073  bpolydif  16076  fprodefsum  16116  demoivreALT  16224  ruclem8  16260  ruclem9  16261  dvdsle  16334  dvdsfac  16350  divalglem7  16423  bitsinv1  16466  sadcadd  16482  sadadd2  16484  saddisjlem  16488  smuval2  16506  smupvallem  16507  smu01lem  16509  smupval  16512  smueqlem  16514  smumullem  16516  bezoutlem4  16566  dfgcd2  16570  rplpwr  16582  nn0seqcvgd  16594  seq1st  16595  alginv  16599  algcvga  16603  algfx  16604  lcmf  16657  prmind2  16709  prmdvdsexp  16739  prmfac1  16744  reumodprminv  16829  pcmpt  16917  pcfac  16924  prmpwdvds  16929  prmreclem4  16944  vdwlem10  17015  ramval  17033  ramcl  17054  cshwrepswhash1  17127  prmlem1a  17131  imasleval  17560  ismre  17607  mreexexd  17665  lubprop  18373  lublecllem  18375  glbprop  18386  joinlem  18398  meetlem  18412  poslubmo  18426  posglbmo  18427  poslubd  18428  isglbd  18524  lubun  18530  mndind  18811  frmdgsum  18845  mulgnnass  19097  mhmmulg  19103  gsumwrev  19354  gsmsymgrfix  19414  gsmsymgreq  19418  psgnunilem3  19482  sylow1lem1  19584  efginvrel2  19713  efgsrel  19720  efgredlemd  19730  efgredlem  19733  efgred  19734  efgrelexlemb  19736  gsum2dlem2  19957  gsumcom2  19961  ablfac1eulem  20060  pgpfac1lem2  20063  pgpfac1lem5  20067  pgpfac1  20068  pgpfac  20072  srgmulgass  20182  srgpcomp  20183  srgbinom  20196  isdomn2OLD  20677  isdomn3  20680  lmodvsmmulgdi  20859  cnfldexp  21372  islindf4  21803  assamulgscm  21866  mplcoe1  22000  mplcoe3  22001  mplcoe5  22003  gsummoncoe1  22251  dmatval  22435  dmatel  22436  dmatmulcl  22443  pmatcoe1fsupp  22644  decpmataa0  22711  decpmatmulsumfsupp  22716  pmatcollpw2lem  22720  pm2mpmhmlem1  22761  fiinopn  22844  mretopd  23035  neiptoptop  23074  cnpfval  23177  iscnp3  23187  tgcn  23195  lmbr  23201  lmbr2  23202  lmbrf  23203  lmss  23241  ishaus  23265  hausnei2  23296  t1sep2  23312  fiuncmp  23347  dfconn2  23362  1stcfb  23388  2ndc1stc  23394  1stcrest  23396  1stcelcls  23404  1stccn  23406  lly1stc  23439  elkgen  23479  kgencn  23499  tx1stc  23593  xkopt  23598  cnmptcom  23621  isr0  23680  r0sep  23691  ptcmpfi  23756  isfildlem  23800  rnelfm  23896  fbflim  23919  flimrest  23926  isflf  23936  flffbas  23938  lmflf  23948  fclsrest  23967  isfcf  23977  cnextfvval  24008  tmdgsum  24038  eltsms  24076  tsmsi  24077  tsmsgsum  24082  tsmssubm  24086  tsmsres  24087  tsmsf1o  24088  isust  24147  isucn  24221  isucn2  24222  ucnima  24224  imasdsf1olem  24317  metss  24452  met1stc  24465  metcnp  24485  metcnpi  24488  metcnpi2  24489  metucn  24515  xrge0tsms  24779  fsumcn  24817  elcncf  24838  cncfi  24843  rescncf  24846  cncfco  24856  caucfil  25240  equivcau  25257  caubl  25265  caublcls  25266  ovolgelb  25438  ovolunlem1a  25454  ovolicc2lem3  25477  voliunlem1  25508  voliunlem3  25510  volsuplem  25513  volsup  25514  dyadmax  25556  vitali  25571  itg2leub  25692  itgfsum  25785  dvnadd  25888  dvnres  25890  cpnord  25894  dvnfre  25913  dvmptfsum  25936  dvferm1  25946  dvferm2  25948  rolle  25951  dvlip  25955  c1lip1  25959  lhop1  25976  deg1leb  26057  ply1divex  26099  fta1g  26132  plyco  26203  dgrcolem1  26236  dgrco  26238  dvnply2  26252  plydivex  26262  aalioulem2  26298  aalioulem3  26299  aalioulem5  26301  aaliou3lem2  26308  dvntaylp  26336  taylthlem1  26338  ulmdvlem3  26368  abelthlem9  26407  cxpmul2  26655  scvxcvx  26953  jensenlem2  26955  jensen  26956  wilthlem3  27037  perfectlem2  27198  bcmono  27245  bposlem5  27256  lgsquad2lem2  27353  addsq2reu  27408  2sqreulem1  27414  2sqreunnlem1  27417  dchrisumlem1  27457  dchrisum0flb  27478  pntpbnd1  27554  pntlemf  27573  qabvle  27593  qabvexp  27594  ostthlem2  27596  ostth2lem2  27602  nosupcbv  27671  nosupno  27672  nosupdm  27673  nosupfv  27675  nosupres  27676  nosupbnd1lem1  27677  nosupbnd1lem3  27679  nosupbnd1lem5  27681  noinfcbv  27686  noinfno  27687  noinfdm  27688  noinffv  27690  noinfres  27691  noinfbnd1lem3  27694  noinfbnd1lem5  27696  eqscut2  27775  addsproplem1  27933  addsprop  27940  negsunif  28018  mulsproplem9  28084  ssltmul2  28108  precsexlem8  28173  precsexlem9  28174  precsexlem11  28176  noseqind  28243  om2noseqrdg  28255  noseqrdgfn  28257  n0addscl  28293  n0mulscl  28294  eucliddivs  28322  peano5uzs  28349  expscllem  28373  expadds  28377  expsne0  28378  expsgt0  28379  pw2cut  28392  tgcgr4  28515  usgr2pth  29751  wlkiswwlks2lem4  29859  wlkiswwlks2  29862  rusgrnumwwlk  29962  clwlkclwwlklem2a  29984  clwlkclwwlklem1  29985  clwlkclwwlkfo  29995  eupth2  30225  frgr3vlem1  30259  3vfriswmgrlem  30263  3vfriswmgr  30264  wlkl0  30353  numclwlk2lem2f1o  30365  isplig  30462  isnvlem  30596  nvi  30600  nmoubi  30758  nmounbi  30762  nmblolbi  30786  ipasslem1  30817  ipassi  30827  hlim2  31178  pjhth  31379  spansni  31543  elspansn2  31553  pjige0  31677  pjcjt2  31678  pjopyth  31706  elcnop  31843  elcnfn  31868  nmopub  31894  cnopc  31899  nmfnleub  31911  elnlfn  31914  cnfnc  31916  nmbdoplb  32011  nmcexi  32012  nmcoplb  32016  lnfnmul  32034  nmbdfnlb  32036  nmcfnlb  32040  pjss2coi  32150  pjssmi  32151  isst  32199  ishst  32200  stcltr1i  32260  mdbr  32280  dmdbr  32285  mddmd2  32295  mdslmd1lem3  32313  mdslmd1lem4  32314  elat2  32326  atcvat2  32375  cdj1i  32419  iuninc  32546  fmptcof2  32640  nn0min  32804  nexple  32828  wrdt2ind  32934  ismnt  32968  xrge0tsmsd  33061  gsumwun  33064  isomnd  33074  omndadd  33079  cyc3genpm  33168  isarchi2  33188  archirng  33191  archiexdiv  33193  archiabl  33201  domnprodn0  33275  isorng  33326  ofldchr  33341  islbs5  33400  unitprodclb  33409  mxidlval  33481  1arithidom  33557  1arithufdlem3  33566  crefeq  33881  esumfzf  34105  issiga  34148  isrnsiga  34149  isldsys  34192  ismeas  34235  isrnmeas  34236  measiun  34254  eulerpartlemn  34418  sseqp1  34432  rrvsum  34491  signsply0  34588  signstfvc  34611  bnj941  34808  bnj106  34904  bnj155  34915  bnj590  34946  bnj591  34947  bnj849  34961  bnj893  34964  bnj944  34974  bnj1128  35026  gblacfnacd  35135  subfacp1lem6  35212  erdszelem8  35225  issconn  35253  cvmliftlem7  35318  cvmliftlem10  35321  cvmlift3lem2  35347  satfsschain  35391  satfrel  35394  satfdm  35396  satfrnmapom  35397  fmlafvel  35412  satffun  35436  mrsubvrs  35549  mclsssvlem  35589  mclsval  35590  mclsax  35596  mclsind  35597  shftvalg  35754  bccolsum  35761  iprodefisumlem  35762  faclimlem1  35765  rdgprc  35817  sbequbidv  36237  cbvsbdavw  36277  fveleq  36474  unblimceq0  36530  bj-ax12  36680  bj-bm1.3ii  37087  rdgeqoa  37393  finxpreclem6  37419  domalom  37427  ralssiun  37430  wl-ax12v2cl  37529  wl-sblimt  37571  wl-sbhbt  37577  wl-2sb6d  37581  wl-mo2df  37593  wl-mo2t  37598  poimirlem2  37651  poimirlem25  37674  poimirlem28  37677  poimirlem31  37680  heicant  37684  mbfresfi  37695  itg2gt0cn  37704  sdclem2  37771  fdc  37774  seqpo  37776  incsequz  37777  mettrifi  37786  prdsbnd2  37824  heiborlem4  37843  bfplem1  37851  iscringd  38027  maxidlval  38068  igenval2  38095  iss2  38367  elrefrels3  38542  ax12eq  38964  ax12el  38965  ax12indalem  38968  ax12inda2ALT  38969  ax12inda  38971  ax12v2-o  38972  riotasvd  38979  isopos  39203  isat3  39330  ishlat1  39375  glbconN  39400  glbconNOLD  39401  ispsubsp  39769  isldil  40134  isltrn  40143  isdilN  40178  trlval  40186  cdleme27b  40392  cdleme29b  40399  cdleme31sn1  40405  cdleme31sn1c  40412  cdleme40v  40493  cdlemk36  40937  cdlemkid5  40959  cdlemn11pre  41234  dihord2pre  41249  islpolN  41507  hdmapffval  41850  hdmapfval  41851  hdmapval2lem  41855  uzindd  41995  sticksstones1  42164  sticksstones2  42165  sticksstones3  42166  sticksstones8  42171  sticksstones10  42173  sticksstones11  42174  sticksstones12a  42175  sticksstones15  42179  indstrd  42211  unitscyglem3  42215  nnaddcom  42286  nnadddir  42288  nnmulcom  42290  eu6w  42674  ismrc  42699  incssnn0  42709  mzpexpmpt  42743  pell14qrexpclnn0  42864  monotuz  42940  rmxypos  42946  jm2.17a  42959  jm2.17b  42960  rmygeid  42963  jm2.18  42987  jm2.19lem3  42990  jm2.25  42998  jm2.15nn0  43002  jm2.16nn0  43003  wepwsolem  43041  aomclem8  43060  dfac11  43061  pwslnm  43093  lnr2i  43115  hbtlem5  43127  cnsrexpcl  43164  rngunsnply  43168  unielss  43217  onsucf1lem  43268  cantnfresb  43323  onmcl  43330  naddonnn  43394  elmapintrab  43575  elmapintab  43595  cnvcnvintabd  43599  eliunov2  43678  relexpxpnnidm  43702  relexpiidm  43703  relexpss1d  43704  iunrelexpmin1  43707  relexpmulnn  43708  iunrelexpmin2  43711  relexp0a  43715  trclimalb2  43725  clsk3nimkb  44039  ntrclsiso  44066  ntrclskb  44068  ntrneiiso  44090  ntrneix2  44092  ntrneixb  44094  gneispace2  44131  gneispacess2  44145  mnuunid  44276  dvgrat  44311  pm14.122b  44422  relpeq1  44944  relpeq3  44946  trfr  44962  pwclaxpow  44984  prclaxpr  44985  uniclaxun  44986  modelac8prim  44992  permaxpow  45009  permaxpr  45010  permaxun  45011  nregmodel  45017  fnchoice  45033  fiiuncl  45069  ssinc  45091  ssdec  45092  wessf1ornlem  45189  dmrelrnrel  45230  fperiodmullem  45312  monoordxrv  45488  fmul01  45589  fmuldfeq  45592  climsuselem1  45616  climinff  45620  ellimcabssub0  45626  limcleqr  45653  addlimc  45657  0ellimcdiv  45658  limclner  45660  limsupref  45694  limsupub  45713  limsupmnf  45730  limsupre2lem  45733  limsupre2  45734  limsupre2mpt  45739  limsupre3lem  45741  limsupre3  45742  limsupre3mpt  45743  xlimbr  45836  cnrefiisplem  45838  dvnmptdivc  45947  dvnmptconst  45950  dvnmul  45952  iblspltprt  45982  itgspltprt  45988  stoweidlem2  46011  stoweidlem3  46012  stoweidlem17  46026  stoweidlem19  46028  stoweidlem21  46030  stoweidlem26  46035  fourierdlem42  46158  issal  46323  ismea  46460  isome  46503  carageniuncllem1  46530  caratheodorylem1  46535  2reu8i  47122  2reuimp0  47123  funressndmafv2rn  47232  2ffzoeq  47336  smonoord  47365  fargshiftf1  47435  ichnfimlem  47457  paireqne  47505  reupr  47516  reuopreuprim  47520  perfectALTVlem2  47716  grimcnv  47881  lmodvsmdi  48334  dmatALTval  48356  dmatALTbasel  48358  snlindsntor  48427  ldepsnlinc  48464  elbigo2r  48513  elbigolo1  48517  itcovalt2  48637  mof0  48796  isnrm4  48885  iscnrm3r  48902  iscnrm4  48908  lubsscl  48914  glbsscl  48915  ipolubdm  48941  ipoglbdm  48944  setrecseq  49529  setrec2fun  49536  setrec2lem2  49538