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  916  19.23t  2218  axc14  2467  mojust  2538  mof  2563  eu6lem  2573  2gencl  3472  3gencl  3473  vtocl2gf  3515  vtocl3gf  3516  vtocl2g  3517  vtocl3g  3518  vtocl2ga  3521  vtocl2gaf  3522  vtocl3gaf  3524  vtocl3ga  3526  vtocl4g  3528  vtocl4ga  3529  eqeu  3652  mo2icl  3660  euind  3670  reu7  3678  reuind  3699  sbctt  3798  sbccomlem  3807  reu8nf  3815  sbcnestgfw  4361  sbcnestgf  4366  r19.36zv  4452  dedth2h  4526  dedth3h  4527  dedth4h  4528  reusngf  4618  reuprg0  4646  preq12bg  4796  elint  4895  elintrabg  4903  intab  4920  axrep1  5213  axreplem  5214  axrep2  5215  axrep6g  5225  bm1.3iiOLD  5237  reusv3  5347  swopolem  5549  solin  5566  freq1  5598  frminex  5610  vtoclr  5694  2optocl  5727  3optocl  5728  raliunxp  5794  resieq  5955  iss  6000  cnveqb  6160  reu3op  6256  reuop  6257  dfpo2  6260  preddowncl  6296  fnbrfvb  6890  fvelimab  6912  fvmptss  6960  fmptco  7082  fprg  7109  fnressn  7112  fressnfv  7114  isoselem  7296  ovg  7532  caovcan  7571  caovordig  7572  caovord  7578  tfisi  7810  tfindsg  7812  tfinds2  7815  tfinds3  7816  dfom2  7819  elom  7820  findsg  7848  finds2  7849  resf1extb  7885  f1o2ndf1  8072  poxp  8078  fnse  8083  xpord3inddlem  8104  soseq  8109  fpr3g  8235  frrlem12  8247  fpr2a  8252  wfr3g  8269  smoeq  8290  smores  8292  smogt  8307  tfrlem1  8315  tfr3  8338  oaordi  8481  oeordi  8523  oeoa  8533  oeoe  8535  nnacl  8547  nnmcl  8548  nnecl  8549  nnacom  8553  nnaordi  8554  nnawordi  8557  nnaass  8558  nndi  8559  nnmass  8560  nnmsucr  8561  nnmcom  8562  nnmordi  8567  naddssim  8621  naddoa  8638  2ecoptocl  8755  3ecoptocl  8756  undifixp  8882  xpdom2g  9011  findcard2  9099  unfi  9105  ssfi  9107  fnfi  9112  fodomfi  9222  imafiOLD  9226  fodomfiOLD  9240  finsschain  9269  marypha1lem  9346  marypha1  9347  supeq1  9358  ordiso2  9430  ordtypelem7  9439  wemaplem1  9461  inf3lem2  9550  inf3lem5  9553  infdiffi  9579  cantnfval2  9590  cantnfle  9592  cantnfp1lem3  9601  oemapval  9604  cantnflem1  9610  cantnf  9614  wemapwe  9618  cnfcom  9621  cnfcom3clem  9626  ttrclss  9641  ttrclselem2  9647  tz9.1  9650  frr3g  9680  frr2  9684  r1pwALT  9770  cplem2  9814  karden  9819  updjud  9858  infxpenc2lem2  9942  fseqenlem1  9946  dfac8clem  9954  alephinit  10017  dfac4  10044  dfac5lem5  10049  dfac2a  10052  dfac2b  10053  dfacacn  10064  dfac12lem3  10068  kmlem2  10074  kmlem13  10085  nnadju  10120  ackbij1lem16  10156  sornom  10199  infpssrlem4  10228  fin23lem14  10255  fin23lem32  10266  fin23lem34  10268  fin23lem36  10270  isf32lem1  10275  isf32lem2  10276  axcc2lem  10358  axcc3  10360  axcclem  10379  zornn0g  10427  ttukeylem5  10435  ttukeylem6  10436  axrepnd  10517  axpowndlem3  10522  zfcndrep  10537  fpwwe2lem7  10560  pwfseqlem3  10583  wunr1om  10642  wunfi  10644  tskr1om  10690  ingru  10738  grudomon  10740  axgroth3  10754  axgroth4  10755  nqereu  10852  mulcanenq  10883  elnp  10910  elnpi  10911  prlem934  10956  infm3  12115  nnindd  12194  nnaddcl  12197  nnmulcl  12198  nnaddcom  12201  nnne0  12211  nnadddir  12233  nnmulcom  12235  peano5uzi  12618  uzind2  12622  nn0indd  12626  zindd  12630  fzindd  12631  uzaddcl  12854  uzwo  12861  indstr  12866  zmax  12895  xmulasslem  13237  xrsupsslem  13259  xrinfmsslem  13260  xrsupss  13261  xrinfmss  13262  flval2  13773  om2uzlti  13912  uzrdgfni  13920  rabssnn0fi  13948  mptnn0fsupp  13959  seqcl2  13982  seqfveq2  13986  seqshft2  13990  monoord  13994  seqsplit  13997  seqcaopr3  13999  seqf1olem2a  14002  seqf1o  14005  seqid2  14010  seqhomo  14011  ser1const  14020  expcllem  14034  expeq0  14054  mulexp  14063  expadd  14066  expmul  14069  expmordi  14129  leexp2r  14136  leexp1a  14137  bernneq  14191  modexp  14200  facdiv  14249  faclbnd  14252  faclbnd4lem4  14258  hashgadd  14339  hashxp  14396  hashmap  14397  hashf1lem2  14418  hashf1  14419  seqcoll  14426  wrdind  14684  wrd2ind  14685  pfxccatin12lem3  14694  cshweqrep  14783  2cshwcshw  14787  relexp0g  14984  relexpsucnnr  14987  relexpsucnnl  14992  relexpcnv  14997  relexpnndm  15003  relexpaddnn  15013  rtrclreclem1  15019  dfrtrclrec2  15020  rtrclreclem2  15021  rtrclreclem4  15023  dfrtrcl2  15024  relexpind  15026  reusq0  15427  rlim  15457  rlim2  15458  rlim0  15470  rlim0lt  15471  rlimi  15475  ello12r  15479  ello1mpt  15483  ello1d  15485  elo12r  15490  lo1o1  15494  o1lo1  15499  lo1res  15521  climshft  15538  o1compt  15549  rlimo1  15579  lo1add  15589  lo1mul  15590  rlimdiv  15608  climub  15624  climserle  15625  caucvgrlem  15635  caurcvgr  15636  iseraltlem2  15645  summolem2a  15677  sumss  15686  fsum2d  15733  fsumabs  15764  fsumrlim  15774  fsumo1  15775  fsumiun  15784  binom  15795  climcndslem1  15814  climcndslem2  15815  cvgrat  15848  clim2prod  15853  prodfn0  15859  prodfrec  15860  ntrivcvgfvn0  15864  prodmolem2a  15899  fprodabs  15939  fprodn0  15944  fprod2d  15946  binomfallfac  16006  bpolycl  16017  bpolydif  16020  fprodefsum  16060  demoivreALT  16168  ruclem8  16204  ruclem9  16205  dvdsle  16279  dvdsfac  16295  divalglem7  16368  bitsinv1  16411  sadcadd  16427  sadadd2  16429  saddisjlem  16433  smuval2  16451  smupvallem  16452  smu01lem  16454  smupval  16457  smueqlem  16459  smumullem  16461  bezoutlem4  16511  dfgcd2  16515  rplpwr  16527  nn0seqcvgd  16539  seq1st  16540  alginv  16544  algcvga  16548  algfx  16549  lcmf  16602  prmind2  16654  prmdvdsexp  16685  prmfac1  16690  reumodprminv  16775  pcmpt  16863  pcfac  16870  prmpwdvds  16875  prmreclem4  16890  vdwlem10  16961  ramval  16979  ramcl  17000  cshwrepswhash1  17073  prmlem1a  17077  imasleval  17505  ismre  17552  mreexexd  17614  lubprop  18322  lublecllem  18324  glbprop  18335  joinlem  18347  meetlem  18361  poslubmo  18375  posglbmo  18376  poslubd  18377  isglbd  18475  lubun  18481  mndind  18796  frmdgsum  18830  mulgnnass  19085  mhmmulg  19091  gsumwrev  19341  gsmsymgrfix  19403  gsmsymgreq  19407  psgnunilem3  19471  sylow1lem1  19573  efginvrel2  19702  efgsrel  19709  efgredlemd  19719  efgredlem  19722  efgred  19723  efgrelexlemb  19725  gsum2dlem2  19946  gsumcom2  19950  ablfac1eulem  20049  pgpfac1lem2  20052  pgpfac1lem5  20056  pgpfac1  20057  pgpfac  20061  isomnd  20098  omndadd  20103  srgmulgass  20198  srgpcomp  20199  srgbinom  20212  isdomn2OLD  20689  isdomn3  20692  isorng  20838  lmodvsmmulgdi  20892  cnfldexp  21385  ofldchr  21556  islindf4  21818  assamulgscm  21881  mplcoe1  22015  mplcoe3  22016  mplcoe5  22018  gsummoncoe1  22273  dmatval  22457  dmatel  22458  dmatmulcl  22465  pmatcoe1fsupp  22666  decpmataa0  22733  decpmatmulsumfsupp  22738  pmatcollpw2lem  22742  pm2mpmhmlem1  22783  fiinopn  22866  mretopd  23057  neiptoptop  23096  cnpfval  23199  iscnp3  23209  tgcn  23217  lmbr  23223  lmbr2  23224  lmbrf  23225  lmss  23263  ishaus  23287  hausnei2  23318  t1sep2  23334  fiuncmp  23369  dfconn2  23384  1stcfb  23410  2ndc1stc  23416  1stcrest  23418  1stcelcls  23426  1stccn  23428  lly1stc  23461  elkgen  23501  kgencn  23521  tx1stc  23615  xkopt  23620  cnmptcom  23643  isr0  23702  r0sep  23713  ptcmpfi  23778  isfildlem  23822  rnelfm  23918  fbflim  23941  flimrest  23948  isflf  23958  flffbas  23960  lmflf  23970  fclsrest  23989  isfcf  23999  cnextfvval  24030  tmdgsum  24060  eltsms  24098  tsmsi  24099  tsmsgsum  24104  tsmssubm  24108  tsmsres  24109  tsmsf1o  24110  isust  24169  isucn  24242  isucn2  24243  ucnima  24245  imasdsf1olem  24338  metss  24473  met1stc  24486  metcnp  24506  metcnpi  24509  metcnpi2  24510  metucn  24536  xrge0tsms  24800  fsumcn  24837  elcncf  24856  cncfi  24861  rescncf  24864  cncfco  24874  caucfil  25250  equivcau  25267  caubl  25275  caublcls  25276  ovolgelb  25447  ovolunlem1a  25463  ovolicc2lem3  25486  voliunlem1  25517  voliunlem3  25519  volsuplem  25522  volsup  25523  dyadmax  25565  vitali  25580  itg2leub  25701  itgfsum  25794  dvnadd  25896  dvnres  25898  cpnord  25902  dvnfre  25919  dvmptfsum  25942  dvferm1  25952  dvferm2  25954  rolle  25957  dvlip  25960  c1lip1  25964  lhop1  25981  deg1leb  26060  ply1divex  26102  fta1g  26135  plyco  26206  dgrcolem1  26238  dgrco  26240  dvnply2  26253  plydivex  26263  aalioulem2  26299  aalioulem3  26300  aalioulem5  26302  aaliou3lem2  26309  dvntaylp  26336  taylthlem1  26338  ulmdvlem3  26367  abelthlem9  26405  cxpmul2  26653  scvxcvx  26949  jensenlem2  26951  jensen  26952  wilthlem3  27033  perfectlem2  27193  bcmono  27240  bposlem5  27251  lgsquad2lem2  27348  addsq2reu  27403  2sqreulem1  27409  2sqreunnlem1  27412  dchrisumlem1  27452  dchrisum0flb  27473  pntpbnd1  27549  pntlemf  27568  qabvle  27588  qabvexp  27589  ostthlem2  27591  ostth2lem2  27597  nosupcbv  27666  nosupno  27667  nosupdm  27668  nosupfv  27670  nosupres  27671  nosupbnd1lem1  27672  nosupbnd1lem3  27674  nosupbnd1lem5  27676  noinfcbv  27681  noinfno  27682  noinfdm  27683  noinffv  27685  noinfres  27686  noinfbnd1lem3  27689  noinfbnd1lem5  27691  eqcuts2  27778  addsproplem1  27961  addsprop  27968  negsunif  28047  mulsproplem9  28116  sltmuls2  28140  precsexlem8  28206  precsexlem9  28207  precsexlem11  28209  noseqind  28284  om2noseqrdg  28296  noseqrdgfn  28298  n0addscl  28336  n0mulscl  28337  eucliddivs  28368  peano5uzs  28396  expscllem  28422  expadds  28427  expsne0  28428  expsgt0  28429  pw2cut  28452  pw2cut2  28454  bdaypw2n0bnd  28456  tgcgr4  28599  usgr2pth  29832  wlkiswwlks2lem4  29940  wlkiswwlks2  29943  rusgrnumwwlk  30046  clwlkclwwlklem2a  30068  clwlkclwwlklem1  30069  clwlkclwwlkfo  30079  eupth2  30309  frgr3vlem1  30343  3vfriswmgrlem  30347  3vfriswmgr  30348  wlkl0  30437  numclwlk2lem2f1o  30449  isplig  30547  isnvlem  30681  nvi  30685  nmoubi  30843  nmounbi  30847  nmblolbi  30871  ipasslem1  30902  ipassi  30912  hlim2  31263  pjhth  31464  spansni  31628  elspansn2  31638  pjige0  31762  pjcjt2  31763  pjopyth  31791  elcnop  31928  elcnfn  31953  nmopub  31979  cnopc  31984  nmfnleub  31996  elnlfn  31999  cnfnc  32001  nmbdoplb  32096  nmcexi  32097  nmcoplb  32101  lnfnmul  32119  nmbdfnlb  32121  nmcfnlb  32125  pjss2coi  32235  pjssmi  32236  isst  32284  ishst  32285  stcltr1i  32345  mdbr  32365  dmdbr  32370  mddmd2  32380  mdslmd1lem3  32398  mdslmd1lem4  32399  elat2  32411  atcvat2  32460  cdj1i  32504  iuninc  32630  fmptcof2  32730  nn0min  32894  nexple  32917  wrdt2ind  33013  ismnt  33043  xrge0tsmsd  33134  gsumwun  33137  cyc3genpm  33213  isarchi2  33246  archirng  33249  archiexdiv  33251  archiabl  33259  domnprodn0  33336  islbs5  33440  unitprodclb  33449  mxidlval  33521  1arithidom  33597  1arithufdlem3  33606  crefeq  33989  esumfzf  34213  issiga  34256  isrnsiga  34257  isldsys  34300  ismeas  34343  isrnmeas  34344  measiun  34362  eulerpartlemn  34525  sseqp1  34539  rrvsum  34598  signsply0  34695  signstfvc  34718  bnj941  34915  bnj106  35010  bnj155  35021  bnj590  35052  bnj591  35053  bnj849  35067  bnj893  35070  bnj944  35080  bnj1128  35132  r1filimi  35246  r1omhfb  35256  tz9.1regs  35278  r1omhfbregs  35281  gblacfnacd  35284  subfacp1lem6  35367  erdszelem8  35380  issconn  35408  cvmliftlem7  35473  cvmliftlem10  35476  cvmlift3lem2  35502  satfsschain  35546  satfrel  35549  satfdm  35551  satfrnmapom  35552  fmlafvel  35567  satffun  35591  mrsubvrs  35704  mclsssvlem  35744  mclsval  35745  mclsax  35751  mclsind  35752  shftvalg  35914  bccolsum  35921  iprodefisumlem  35922  faclimlem1  35925  rdgprc  35974  sbequbidv  36396  cbvsbdavw  36436  fveleq  36633  dfttc4lem1  36710  dfttc4  36712  elttcirr  36713  regsfromregtco  36720  mh-unprimbi  36726  unblimceq0  36767  bj-ax12  36951  bj-bm1.3ii  37371  rdgeqoa  37686  finxpreclem6  37712  domalom  37720  ralssiun  37723  wl-ax12v2cl  37822  wl-sblimt  37873  wl-sbhbt  37879  wl-2sb6d  37883  wl-mo2df  37895  wl-mo2t  37900  poimirlem2  37943  poimirlem25  37966  poimirlem28  37969  poimirlem31  37972  heicant  37976  mbfresfi  37987  itg2gt0cn  37996  sdclem2  38063  fdc  38066  seqpo  38068  incsequz  38069  mettrifi  38078  prdsbnd2  38116  heiborlem4  38135  bfplem1  38143  iscringd  38319  maxidlval  38360  igenval2  38387  iss2  38665  elrefrels3  38920  ax12eq  39387  ax12el  39388  ax12indalem  39391  ax12inda2ALT  39392  ax12inda  39394  ax12v2-o  39395  riotasvd  39402  isopos  39626  isat3  39753  ishlat1  39798  glbconN  39823  ispsubsp  40191  isldil  40556  isltrn  40565  isdilN  40600  trlval  40608  cdleme27b  40814  cdleme29b  40821  cdleme31sn1  40827  cdleme31sn1c  40834  cdleme40v  40915  cdlemk36  41359  cdlemkid5  41381  cdlemn11pre  41656  dihord2pre  41671  islpolN  41929  hdmapffval  42272  hdmapfval  42273  hdmapval2lem  42277  uzindd  42417  sticksstones1  42585  sticksstones2  42586  sticksstones3  42587  sticksstones8  42592  sticksstones10  42594  sticksstones11  42595  sticksstones12a  42596  sticksstones15  42600  indstrd  42632  unitscyglem3  42636  eu6w  43109  ismrc  43133  incssnn0  43143  mzpexpmpt  43177  pell14qrexpclnn0  43294  monotuz  43369  rmxypos  43375  jm2.17a  43388  jm2.17b  43389  rmygeid  43392  jm2.18  43416  jm2.19lem3  43419  jm2.25  43427  jm2.15nn0  43431  jm2.16nn0  43432  wepwsolem  43470  aomclem8  43489  dfac11  43490  pwslnm  43522  lnr2i  43544  hbtlem5  43556  cnsrexpcl  43593  rngunsnply  43597  unielss  43646  onsucf1lem  43697  cantnfresb  43752  onmcl  43759  naddonnn  43823  elmapintrab  44003  elmapintab  44023  cnvcnvintabd  44027  eliunov2  44106  relexpxpnnidm  44130  relexpiidm  44131  relexpss1d  44132  iunrelexpmin1  44135  relexpmulnn  44136  iunrelexpmin2  44139  relexp0a  44143  trclimalb2  44153  clsk3nimkb  44467  ntrclsiso  44494  ntrclskb  44496  ntrneiiso  44518  ntrneix2  44520  ntrneixb  44522  gneispace2  44559  gneispacess2  44573  mnuunid  44704  dvgrat  44739  pm14.122b  44850  relpeq1  45371  relpeq3  45373  trfr  45389  pwclaxpow  45411  prclaxpr  45412  uniclaxun  45413  modelac8prim  45419  permaxpow  45436  permaxpr  45437  permaxun  45438  nregmodel  45444  fnchoice  45460  fiiuncl  45496  ssinc  45517  ssdec  45518  wessf1ornlem  45615  dmrelrnrel  45655  fperiodmullem  45736  monoordxrv  45909  fmul01  46010  fmuldfeq  46013  climsuselem1  46037  climinff  46041  ellimcabssub0  46047  limcleqr  46072  addlimc  46076  0ellimcdiv  46077  limclner  46079  limsupref  46113  limsupub  46132  limsupmnf  46149  limsupre2lem  46152  limsupre2  46153  limsupre2mpt  46158  limsupre3lem  46160  limsupre3  46161  limsupre3mpt  46162  xlimbr  46255  cnrefiisplem  46257  dvnmptdivc  46366  dvnmptconst  46369  dvnmul  46371  iblspltprt  46401  itgspltprt  46407  stoweidlem2  46430  stoweidlem3  46431  stoweidlem17  46445  stoweidlem19  46447  stoweidlem21  46449  stoweidlem26  46454  fourierdlem42  46577  issal  46742  ismea  46879  isome  46922  carageniuncllem1  46949  caratheodorylem1  46954  2reu8i  47561  2reuimp0  47562  funressndmafv2rn  47671  2ffzoeq  47776  smonoord  47825  fargshiftf1  47901  ichnfimlem  47923  paireqne  47971  reupr  47982  reuopreuprim  47986  perfectALTVlem2  48198  grimcnv  48364  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem4  48595  pgnbgreunbgr  48601  lmodvsmdi  48855  dmatALTval  48876  dmatALTbasel  48878  snlindsntor  48947  ldepsnlinc  48984  elbigo2r  49029  elbigolo1  49033  itcovalt2  49153  mof0  49313  isnrm4  49406  iscnrm3r  49423  iscnrm4  49429  lubsscl  49435  glbsscl  49436  ipolubdm  49462  ipoglbdm  49465  setrecseq  50160  setrec2fun  50167  setrec2lem2  50169