Theorem imbi2d 341

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 274	1 ⊢ (𝜑 → ((𝜃 → 𝜓) ↔ (𝜃 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  imbi12d  345  imbi2  349  pm5.42  548  orbi2d  921  19.23t  2222  axc14  2471  mojust  2542  mof  2567  eu6lem  2577  2gencl  3473  3gencl  3474  vtocl2gf  3515  vtocl3gf  3516  vtocl2g  3517  vtocl3g  3518  vtocl2ga  3521  vtocl2gaf  3522  vtocl3gaf  3523  vtocl3ga  3524  vtocl4g  3525  vtocl4ga  3526  eqeu  3647  mo2icl  3655  euind  3665  reu7  3673  reuind  3694  sbctt  3792  sbccomlem  3801  reu8nf  3809  sbcnestgfw  4349  sbcnestgf  4354  r19.36zv  4440  dedth2h  4514  dedth3h  4515  dedth4h  4516  reusngf  4606  reuprg0  4634  preq12bg  4784  elint  4883  elintrabg  4891  intab  4908  axrep1  5200  axreplem  5201  axrep2  5202  axrep6g  5212  bm1.3iiOLD  5224  reusv3  5334  swopolem  5536  solin  5553  freq1  5585  frminex  5597  vtoclr  5681  2optocl  5714  3optocl  5715  raliunxp  5781  resieq  5942  iss  5987  cnveqb  6147  reu3op  6243  reuop  6244  dfpo2  6247  preddowncl  6283  fnbrfvb  6877  fvelimab  6899  fvmptss  6948  fmptco  7071  fprg  7098  fnressn  7101  fressnfv  7103  isoselem  7285  ovg  7521  caovcan  7560  caovordig  7561  caovord  7567  tfisi  7799  tfindsg  7801  tfinds2  7804  tfinds3  7805  dfom2  7808  elom  7809  findsg  7837  finds2  7838  resf1extb  7874  f1o2ndf1  8061  poxp  8068  fnse  8073  xpord3inddlem  8094  soseq  8099  fpr3g  8225  frrlem12  8237  fpr2a  8242  wfr3g  8259  smoeq  8280  smores  8282  smogt  8297  tfrlem1  8305  tfr3  8328  oaordi  8471  oeordi  8513  oeoa  8523  oeoe  8525  nnacl  8537  nnmcl  8538  nnecl  8539  nnacom  8543  nnaordi  8544  nnawordi  8547  nnaass  8548  nndi  8549  nnmass  8550  nnmsucr  8551  nnmcom  8552  nnmordi  8557  naddssim  8611  naddoa  8628  2ecoptocl  8745  3ecoptocl  8746  undifixp  8872  xpdom2g  9001  findcard2  9089  unfi  9095  ssfi  9097  fnfi  9102  fodomfi  9212  imafiOLD  9216  fodomfiOLD  9230  finsschain  9259  marypha1lem  9336  marypha1  9337  supeq1  9348  ordiso2  9420  ordtypelem7  9429  wemaplem1  9451  inf3lem2  9541  inf3lem5  9544  infdiffi  9570  cantnfval2  9581  cantnfle  9583  cantnfp1lem3  9592  oemapval  9595  cantnflem1  9601  cantnf  9605  wemapwe  9609  cnfcom  9612  cnfcom3clem  9617  ttrclss  9632  ttrclselem2  9638  tz9.1  9641  frr3g  9671  frr2  9675  r1pwALT  9761  cplem2  9805  karden  9810  updjud  9849  infxpenc2lem2  9933  fseqenlem1  9937  dfac8clem  9945  alephinit  10008  dfac4  10035  dfac5lem5  10040  dfac2a  10043  dfac2b  10044  dfacacn  10055  dfac12lem3  10059  kmlem2  10065  kmlem13  10076  nnadju  10111  ackbij1lem16  10147  sornom  10190  infpssrlem4  10219  fin23lem14  10246  fin23lem32  10257  fin23lem34  10259  fin23lem36  10261  isf32lem1  10266  isf32lem2  10267  axcc2lem  10349  axcc3  10351  axcclem  10370  zornn0g  10418  ttukeylem5  10426  ttukeylem6  10427  axrepnd  10508  axpowndlem3  10513  zfcndrep  10528  fpwwe2lem7  10551  pwfseqlem3  10574  wunr1om  10633  wunfi  10635  tskr1om  10681  ingru  10729  grudomon  10731  axgroth3  10745  axgroth4  10746  nqereu  10843  mulcanenq  10874  elnp  10901  elnpi  10902  prlem934  10947  infm3  12106  nnindd  12185  nnaddcl  12188  nnmulcl  12189  nnaddcom  12192  nnne0  12202  nnadddir  12224  nnmulcom  12226  peano5uzi  12609  uzind2  12613  nn0indd  12617  zindd  12621  fzindd  12622  uzaddcl  12845  uzwo  12852  indstr  12857  zmax  12886  xmulasslem  13228  xrsupsslem  13250  xrinfmsslem  13251  xrsupss  13252  xrinfmss  13253  flval2  13764  om2uzlti  13903  uzrdgfni  13911  rabssnn0fi  13939  mptnn0fsupp  13950  seqcl2  13973  seqfveq2  13977  seqshft2  13981  monoord  13985  seqsplit  13988  seqcaopr3  13990  seqf1olem2a  13993  seqf1o  13996  seqid2  14001  seqhomo  14002  ser1const  14011  expcllem  14025  expeq0  14045  mulexp  14054  expadd  14057  expmul  14060  expmordi  14120  leexp2r  14127  leexp1a  14128  bernneq  14182  modexp  14191  facdiv  14240  faclbnd  14243  faclbnd4lem4  14249  hashgadd  14330  hashxp  14387  hashmap  14388  hashf1lem2  14409  hashf1  14410  seqcoll  14417  wrdind  14675  wrd2ind  14676  pfxccatin12lem3  14685  cshweqrep  14774  2cshwcshw  14778  relexp0g  14975  relexpsucnnr  14978  relexpsucnnl  14983  relexpcnv  14988  relexpnndm  14994  relexpaddnn  15004  rtrclreclem1  15010  dfrtrclrec2  15011  rtrclreclem2  15012  rtrclreclem4  15014  dfrtrcl2  15015  relexpind  15017  reusq0  15418  rlim  15448  rlim2  15449  rlim0  15461  rlim0lt  15462  rlimi  15466  ello12r  15470  ello1mpt  15474  ello1d  15476  elo12r  15481  lo1o1  15485  o1lo1  15490  lo1res  15512  climshft  15529  o1compt  15540  rlimo1  15570  lo1add  15580  lo1mul  15581  rlimdiv  15599  climub  15615  climserle  15616  caucvgrlem  15626  caurcvgr  15627  iseraltlem2  15636  summolem2a  15668  sumss  15677  fsum2d  15724  fsumabs  15755  fsumrlim  15765  fsumo1  15766  fsumiun  15775  binom  15786  climcndslem1  15805  climcndslem2  15806  cvgrat  15839  clim2prod  15844  prodfn0  15850  prodfrec  15851  ntrivcvgfvn0  15855  prodmolem2a  15890  fprodabs  15930  fprodn0  15935  fprod2d  15937  binomfallfac  15997  bpolycl  16008  bpolydif  16011  fprodefsum  16051  demoivreALT  16159  ruclem8  16195  ruclem9  16196  dvdsle  16270  dvdsfac  16286  divalglem7  16359  bitsinv1  16402  sadcadd  16418  sadadd2  16420  saddisjlem  16424  smuval2  16442  smupvallem  16443  smu01lem  16445  smupval  16448  smueqlem  16450  smumullem  16452  bezoutlem4  16502  dfgcd2  16506  rplpwr  16518  nn0seqcvgd  16530  seq1st  16531  alginv  16535  algcvga  16539  algfx  16540  lcmf  16593  prmind2  16645  prmdvdsexp  16676  prmfac1  16681  reumodprminv  16766  pcmpt  16854  pcfac  16861  prmpwdvds  16866  prmreclem4  16881  vdwlem10  16952  ramval  16970  ramcl  16991  cshwrepswhash1  17064  prmlem1a  17068  imasleval  17496  ismre  17543  mreexexd  17605  lubprop  18313  lublecllem  18315  glbprop  18326  joinlem  18338  meetlem  18352  poslubmo  18366  posglbmo  18367  poslubd  18368  isglbd  18466  lubun  18472  mndind  18787  frmdgsum  18821  mulgnnass  19076  mhmmulg  19082  gsumwrev  19332  gsmsymgrfix  19394  gsmsymgreq  19398  psgnunilem3  19462  sylow1lem1  19564  efginvrel2  19693  efgsrel  19700  efgredlemd  19710  efgredlem  19713  efgred  19714  efgrelexlemb  19716  gsum2dlem2  19937  gsumcom2  19941  ablfac1eulem  20040  pgpfac1lem2  20043  pgpfac1lem5  20047  pgpfac1  20048  pgpfac  20052  isomnd  20089  omndadd  20094  srgmulgass  20189  srgpcomp  20190  srgbinom  20203  isdomn2OLD  20684  isdomn3  20687  isorng  20833  lmodvsmmulgdi  20887  cnfldexp  21380  ofldchr  21551  islindf4  21813  assamulgscm  21876  mplcoe1  22013  mplcoe3  22014  mplcoe5  22016  gsummoncoe1  22294  dmatval  22475  dmatel  22476  dmatmulcl  22483  pmatcoe1fsupp  22684  decpmataa0  22751  decpmatmulsumfsupp  22756  pmatcollpw2lem  22760  pm2mpmhmlem1  22801  fiinopn  22884  mretopd  23075  neiptoptop  23114  cnpfval  23217  iscnp3  23227  tgcn  23235  lmbr  23241  lmbr2  23242  lmbrf  23243  lmss  23281  ishaus  23305  hausnei2  23336  t1sep2  23352  fiuncmp  23387  dfconn2  23402  1stcfb  23428  2ndc1stc  23434  1stcrest  23436  1stcelcls  23444  1stccn  23446  lly1stc  23479  elkgen  23519  kgencn  23539  tx1stc  23633  xkopt  23638  cnmptcom  23661  isr0  23720  r0sep  23731  ptcmpfi  23796  isfildlem  23840  rnelfm  23936  fbflim  23959  flimrest  23966  isflf  23976  flffbas  23978  lmflf  23988  fclsrest  24007  isfcf  24017  cnextfvval  24048  tmdgsum  24078  eltsms  24116  tsmsi  24117  tsmsgsum  24122  tsmssubm  24126  tsmsres  24127  tsmsf1o  24128  isust  24187  isucn  24260  isucn2  24261  ucnima  24263  imasdsf1olem  24356  metss  24491  met1stc  24504  metcnp  24524  metcnpi  24527  metcnpi2  24528  metucn  24554  xrge0tsms  24818  fsumcn  24855  elcncf  24874  cncfi  24879  rescncf  24882  cncfco  24892  caucfil  25268  equivcau  25285  caubl  25293  caublcls  25294  ovolgelb  25465  ovolunlem1a  25481  ovolicc2lem3  25504  voliunlem1  25535  voliunlem3  25537  volsuplem  25540  volsup  25541  dyadmax  25583  vitali  25598  itg2leub  25719  itgfsum  25812  dvnadd  25914  dvnres  25916  cpnord  25920  dvnfre  25937  dvmptfsum  25960  dvferm1  25970  dvferm2  25972  rolle  25975  dvlip  25978  c1lip1  25982  lhop1  25999  deg1leb  26078  ply1divex  26120  fta1g  26153  plyco  26224  dgrcolem1  26256  dgrco  26258  dvnply2  26271  plydivex  26281  aalioulem2  26317  aalioulem3  26318  aalioulem5  26320  aaliou3lem2  26327  dvntaylp  26354  taylthlem1  26356  ulmdvlem3  26385  abelthlem9  26423  cxpmul2  26671  scvxcvx  26967  jensenlem2  26969  jensen  26970  wilthlem3  27051  perfectlem2  27211  bcmono  27258  bposlem5  27269  lgsquad2lem2  27366  addsq2reu  27421  2sqreulem1  27427  2sqreunnlem1  27430  dchrisumlem1  27470  dchrisum0flb  27491  pntpbnd1  27567  pntlemf  27586  qabvle  27606  qabvexp  27607  ostthlem2  27609  ostth2lem2  27615  nosupcbv  27684  nosupno  27685  nosupdm  27686  nosupfv  27688  nosupres  27689  nosupbnd1lem1  27690  nosupbnd1lem3  27692  nosupbnd1lem5  27694  noinfcbv  27699  noinfno  27700  noinfdm  27701  noinffv  27703  noinfres  27704  noinfbnd1lem3  27707  noinfbnd1lem5  27709  eqcuts2  27796  addsproplem1  27979  addsprop  27986  negsunif  28065  mulsproplem9  28134  sltmuls2  28158  precsexlem8  28224  precsexlem9  28225  precsexlem11  28227  noseqind  28302  om2noseqrdg  28314  noseqrdgfn  28316  n0addscl  28354  n0mulscl  28355  eucliddivs  28386  peano5uzs  28414  expscllem  28440  expadds  28445  expsne0  28446  expsgt0  28447  pw2cut  28470  pw2cut2  28472  bdaypw2n0bnd  28474  tgcgr4  28617  usgr2pth  29850  wlkiswwlks2lem4  29958  wlkiswwlks2  29961  rusgrnumwwlk  30064  clwlkclwwlklem2a  30086  clwlkclwwlklem1  30087  clwlkclwwlkfo  30097  eupth2  30327  frgr3vlem1  30361  3vfriswmgrlem  30365  3vfriswmgr  30366  wlkl0  30455  numclwlk2lem2f1o  30467  isplig  30565  isnvlem  30699  nvi  30703  nmoubi  30861  nmounbi  30865  nmblolbi  30889  ipasslem1  30920  ipassi  30930  hlim2  31281  pjhth  31482  spansni  31646  elspansn2  31656  pjige0  31780  pjcjt2  31781  pjopyth  31809  elcnop  31946  elcnfn  31971  nmopub  31997  cnopc  32002  nmfnleub  32014  elnlfn  32017  cnfnc  32019  nmbdoplb  32114  nmcexi  32115  nmcoplb  32119  lnfnmul  32137  nmbdfnlb  32139  nmcfnlb  32143  pjss2coi  32253  pjssmi  32254  isst  32302  ishst  32303  stcltr1i  32363  mdbr  32383  dmdbr  32388  mddmd2  32398  mdslmd1lem3  32416  mdslmd1lem4  32417  elat2  32429  atcvat2  32478  cdj1i  32522  iuninc  32649  fmptcof2  32749  nn0min  32913  nexple  32936  wrdt2ind  33032  ismnt  33062  xrge0tsmsd  33154  gsumwun  33157  cyc3genpm  33233  isarchi2  33266  archirng  33269  archiexdiv  33271  archiabl  33279  domnprodn0  33356  islbs5  33463  unitprodclb  33472  mxidlval  33544  1arithidom  33620  1arithufdlem3  33629  crefeq  34029  esumfzf  34253  issiga  34296  isrnsiga  34297  isldsys  34340  ismeas  34383  isrnmeas  34384  measiun  34402  eulerpartlemn  34565  sseqp1  34579  rrvsum  34638  signsply0  34735  signstfvc  34758  bnj941  34955  bnj106  35050  bnj155  35061  bnj590  35092  bnj591  35093  bnj849  35107  bnj893  35110  bnj944  35120  bnj1128  35172  r1filimi  35284  r1omhfb  35293  tz9.1regs  35315  r1omhfbregs  35318  gblacfnacd  35330  subfacp1lem6  35413  erdszelem8  35426  issconn  35454  cvmliftlem7  35519  cvmliftlem10  35522  cvmlift3lem2  35548  satfsschain  35592  satfrel  35595  satfdm  35597  satfrnmapom  35598  fmlafvel  35613  satffun  35637  mrsubvrs  35750  mclsssvlem  35790  mclsval  35791  mclsax  35797  mclsind  35798  shftvalg  35960  bccolsum  35967  iprodefisumlem  35968  faclimlem1  35971  rdgprc  36020  sbequbidv  36442  cbvsbdavw  36482  fveleq  36679  dfttc4lem1  36756  dfttc4  36758  elttcirr  36759  regsfromregtco  36766  mh-unprimbi  36772  unblimceq0  36813  bj-ax12  36997  bj-bm1.3ii  37417  rdgeqoa  37732  finxpreclem6  37758  domalom  37766  ralssiun  37769  wl-ax12v2cl  37868  wl-sblimt  37919  wl-sbhbt  37925  wl-2sb6d  37929  wl-mo2df  37941  wl-mo2t  37946  poimirlem2  37989  poimirlem25  38012  poimirlem28  38015  poimirlem31  38018  heicant  38022  mbfresfi  38033  itg2gt0cn  38042  sdclem2  38109  fdc  38112  seqpo  38114  incsequz  38115  mettrifi  38124  prdsbnd2  38162  heiborlem4  38181  bfplem1  38189  iscringd  38365  maxidlval  38406  igenval2  38433  iss2  38711  elrefrels3  38966  ax12eq  39433  ax12el  39434  ax12indalem  39437  ax12inda2ALT  39438  ax12inda  39440  ax12v2-o  39441  riotasvd  39448  isopos  39672  isat3  39799  ishlat1  39844  glbconN  39869  ispsubsp  40237  isldil  40602  isltrn  40611  isdilN  40646  trlval  40654  cdleme27b  40860  cdleme29b  40867  cdleme31sn1  40873  cdleme31sn1c  40880  cdleme40v  40961  cdlemk36  41405  cdlemkid5  41427  cdlemn11pre  41702  dihord2pre  41717  islpolN  41975  hdmapffval  42318  hdmapfval  42319  hdmapval2lem  42323  uzindd  42463  sticksstones1  42631  sticksstones2  42632  sticksstones3  42633  sticksstones8  42638  sticksstones10  42640  sticksstones11  42641  sticksstones12a  42642  sticksstones15  42646  indstrd  42678  unitscyglem3  42682  eu6w  43126  ismrc  43150  incssnn0  43160  mzpexpmpt  43194  pell14qrexpclnn0  43311  monotuz  43386  rmxypos  43392  jm2.17a  43405  jm2.17b  43406  rmygeid  43409  jm2.18  43433  jm2.19lem3  43436  jm2.25  43444  jm2.15nn0  43448  jm2.16nn0  43449  wepwsolem  43487  aomclem8  43506  dfac11  43507  pwslnm  43539  lnr2i  43561  hbtlem5  43573  cnsrexpcl  43610  rngunsnply  43614  unielss  43663  onsucf1lem  43714  cantnfresb  43769  onmcl  43776  naddonnn  43840  elmapintrab  44020  elmapintab  44040  cnvcnvintabd  44044  eliunov2  44123  relexpxpnnidm  44147  relexpiidm  44148  relexpss1d  44149  iunrelexpmin1  44152  relexpmulnn  44153  iunrelexpmin2  44156  relexp0a  44160  trclimalb2  44170  clsk3nimkb  44484  ntrclsiso  44511  ntrclskb  44513  ntrneiiso  44535  ntrneix2  44537  ntrneixb  44539  gneispace2  44576  gneispacess2  44590  mnuunid  44721  dvgrat  44756  pm14.122b  44867  relpeq1  45388  relpeq3  45390  trfr  45406  pwclaxpow  45428  prclaxpr  45429  uniclaxun  45430  modelac8prim  45436  permaxpow  45453  permaxpr  45454  permaxun  45455  nregmodel  45461  fnchoice  45477  fiiuncl  45513  ssinc  45534  ssdec  45535  wessf1ornlem  45632  dmrelrnrel  45671  fperiodmullem  45751  monoordxrv  45924  fmul01  46025  fmuldfeq  46028  climsuselem1  46052  climinff  46056  ellimcabssub0  46062  limcleqr  46087  addlimc  46091  0ellimcdiv  46092  limclner  46094  limsupref  46128  limsupub  46147  limsupmnf  46164  limsupre2lem  46167  limsupre2  46168  limsupre2mpt  46173  limsupre3lem  46175  limsupre3  46176  limsupre3mpt  46177  xlimbr  46270  cnrefiisplem  46272  dvnmptdivc  46381  dvnmptconst  46384  dvnmul  46386  iblspltprt  46416  itgspltprt  46422  stoweidlem2  46445  stoweidlem3  46446  stoweidlem17  46460  stoweidlem19  46462  stoweidlem21  46464  stoweidlem26  46469  fourierdlem42  46592  issal  46757  ismea  46894  isome  46937  carageniuncllem1  46964  caratheodorylem1  46969  2reu8i  47576  2reuimp0  47577  funressndmafv2rn  47686  2ffzoeq  47791  smonoord  47840  fargshiftf1  47916  ichnfimlem  47938  paireqne  47986  reupr  47997  reuopreuprim  48001  perfectALTVlem2  48213  grimcnv  48379  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem4  48610  pgnbgreunbgr  48616  lmodvsmdi  48870  dmatALTval  48891  dmatALTbasel  48893  snlindsntor  48962  ldepsnlinc  48999  elbigo2r  49044  elbigolo1  49048  itcovalt2  49168  mof0  49328  isnrm4  49421  iscnrm3r  49438  iscnrm4  49444  lubsscl  49450  glbsscl  49451  ipolubdm  49477  ipoglbdm  49480  setrecseq  50175  setrec2fun  50182  setrec2lem2  50184