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  2217  axc14  2467  mojust  2538  mof  2563  eu6lem  2573  2gencl  3483  3gencl  3484  vtocl2gf  3527  vtocl3gf  3528  vtocl2g  3529  vtocl3g  3530  vtocl2ga  3533  vtocl2gaf  3534  vtocl3gaf  3536  vtocl3ga  3538  vtocl4g  3540  vtocl4ga  3541  eqeu  3664  mo2icl  3672  euind  3682  reu7  3690  reuind  3711  sbctt  3810  sbccomlem  3819  reu8nf  3827  sbcnestgfw  4373  sbcnestgf  4378  r19.36zv  4465  dedth2h  4539  dedth3h  4540  dedth4h  4541  reusngf  4631  reuprg0  4659  preq12bg  4809  elint  4908  elintrabg  4916  intab  4933  axrep1  5225  axreplem  5226  axrep2  5227  axrep6g  5235  bm1.3iiOLD  5247  reusv3  5350  swopolem  5542  solin  5559  freq1  5591  frminex  5603  vtoclr  5687  2optocl  5720  3optocl  5721  raliunxp  5788  resieq  5949  iss  5994  cnveqb  6154  reu3op  6250  reuop  6251  dfpo2  6254  preddowncl  6290  fnbrfvb  6884  fvelimab  6906  fvmptss  6953  fmptco  7074  fprg  7100  fnressn  7103  fressnfv  7105  isoselem  7287  ovg  7523  caovcan  7562  caovordig  7563  caovord  7569  tfisi  7801  tfindsg  7803  tfinds2  7806  tfinds3  7807  dfom2  7810  elom  7811  findsg  7839  finds2  7840  resf1extb  7876  f1o2ndf1  8064  poxp  8070  fnse  8075  xpord3inddlem  8096  soseq  8101  fpr3g  8227  frrlem12  8239  fpr2a  8244  wfr3g  8261  smoeq  8282  smores  8284  smogt  8299  tfrlem1  8307  tfr3  8330  oaordi  8473  oeordi  8515  oeoa  8525  oeoe  8527  nnacl  8539  nnmcl  8540  nnecl  8541  nnacom  8545  nnaordi  8546  nnawordi  8549  nnaass  8550  nndi  8551  nnmass  8552  nnmsucr  8553  nnmcom  8554  nnmordi  8559  naddssim  8613  naddoa  8630  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  9538  inf3lem5  9541  infdiffi  9567  cantnfval2  9578  cantnfle  9580  cantnfp1lem3  9589  oemapval  9592  cantnflem1  9598  cantnf  9602  wemapwe  9606  cnfcom  9609  cnfcom3clem  9614  ttrclss  9629  ttrclselem2  9635  tz9.1  9638  frr3g  9668  frr2  9672  r1pwALT  9758  cplem2  9802  karden  9807  updjud  9846  infxpenc2lem2  9930  fseqenlem1  9934  dfac8clem  9942  alephinit  10005  dfac4  10032  dfac5lem5  10037  dfac2a  10040  dfac2b  10041  dfacacn  10052  dfac12lem3  10056  kmlem2  10062  kmlem13  10073  nnadju  10108  ackbij1lem16  10144  sornom  10187  infpssrlem4  10216  fin23lem14  10243  fin23lem32  10254  fin23lem34  10256  fin23lem36  10258  isf32lem1  10263  isf32lem2  10264  axcc2lem  10346  axcc3  10348  axcclem  10367  zornn0g  10415  ttukeylem5  10423  ttukeylem6  10424  axrepnd  10505  axpowndlem3  10510  zfcndrep  10525  fpwwe2lem7  10548  pwfseqlem3  10571  wunr1om  10630  wunfi  10632  tskr1om  10678  ingru  10726  grudomon  10728  axgroth3  10742  axgroth4  10743  nqereu  10840  mulcanenq  10871  elnp  10898  elnpi  10899  prlem934  10944  infm3  12101  nnindd  12165  nnaddcl  12168  nnmulcl  12169  nnne0  12179  peano5uzi  12581  uzind2  12585  nn0indd  12589  zindd  12593  fzindd  12594  uzaddcl  12817  uzwo  12824  indstr  12829  zmax  12858  xmulasslem  13200  xrsupsslem  13222  xrinfmsslem  13223  xrsupss  13224  xrinfmss  13225  flval2  13734  om2uzlti  13873  uzrdgfni  13881  rabssnn0fi  13909  mptnn0fsupp  13920  seqcl2  13943  seqfveq2  13947  seqshft2  13951  monoord  13955  seqsplit  13958  seqcaopr3  13960  seqf1olem2a  13963  seqf1o  13966  seqid2  13971  seqhomo  13972  ser1const  13981  expcllem  13995  expeq0  14015  mulexp  14024  expadd  14027  expmul  14030  expmordi  14090  leexp2r  14097  leexp1a  14098  bernneq  14152  modexp  14161  facdiv  14210  faclbnd  14213  faclbnd4lem4  14219  hashgadd  14300  hashxp  14357  hashmap  14358  hashf1lem2  14379  hashf1  14380  seqcoll  14387  wrdind  14645  wrd2ind  14646  pfxccatin12lem3  14655  cshweqrep  14744  2cshwcshw  14748  relexp0g  14945  relexpsucnnr  14948  relexpsucnnl  14953  relexpcnv  14958  relexpnndm  14964  relexpaddnn  14974  rtrclreclem1  14980  dfrtrclrec2  14981  rtrclreclem2  14982  rtrclreclem4  14984  dfrtrcl2  14985  relexpind  14987  reusq0  15388  rlim  15418  rlim2  15419  rlim0  15431  rlim0lt  15432  rlimi  15436  ello12r  15440  ello1mpt  15444  ello1d  15446  elo12r  15451  lo1o1  15455  o1lo1  15460  lo1res  15482  climshft  15499  o1compt  15510  rlimo1  15540  lo1add  15550  lo1mul  15551  rlimdiv  15569  climub  15585  climserle  15586  caucvgrlem  15596  caurcvgr  15597  iseraltlem2  15606  summolem2a  15638  sumss  15647  fsum2d  15694  fsumabs  15724  fsumrlim  15734  fsumo1  15735  fsumiun  15744  binom  15753  climcndslem1  15772  climcndslem2  15773  cvgrat  15806  clim2prod  15811  prodfn0  15817  prodfrec  15818  ntrivcvgfvn0  15822  prodmolem2a  15857  fprodabs  15897  fprodn0  15902  fprod2d  15904  binomfallfac  15964  bpolycl  15975  bpolydif  15978  fprodefsum  16018  demoivreALT  16126  ruclem8  16162  ruclem9  16163  dvdsle  16237  dvdsfac  16253  divalglem7  16326  bitsinv1  16369  sadcadd  16385  sadadd2  16387  saddisjlem  16391  smuval2  16409  smupvallem  16410  smu01lem  16412  smupval  16415  smueqlem  16417  smumullem  16419  bezoutlem4  16469  dfgcd2  16473  rplpwr  16485  nn0seqcvgd  16497  seq1st  16498  alginv  16502  algcvga  16506  algfx  16507  lcmf  16560  prmind2  16612  prmdvdsexp  16642  prmfac1  16647  reumodprminv  16732  pcmpt  16820  pcfac  16827  prmpwdvds  16832  prmreclem4  16847  vdwlem10  16918  ramval  16936  ramcl  16957  cshwrepswhash1  17030  prmlem1a  17034  imasleval  17462  ismre  17509  mreexexd  17571  lubprop  18279  lublecllem  18281  glbprop  18292  joinlem  18304  meetlem  18318  poslubmo  18332  posglbmo  18333  poslubd  18334  isglbd  18432  lubun  18438  mndind  18753  frmdgsum  18787  mulgnnass  19039  mhmmulg  19045  gsumwrev  19295  gsmsymgrfix  19357  gsmsymgreq  19361  psgnunilem3  19425  sylow1lem1  19527  efginvrel2  19656  efgsrel  19663  efgredlemd  19673  efgredlem  19676  efgred  19677  efgrelexlemb  19679  gsum2dlem2  19900  gsumcom2  19904  ablfac1eulem  20003  pgpfac1lem2  20006  pgpfac1lem5  20010  pgpfac1  20011  pgpfac  20015  isomnd  20052  omndadd  20057  srgmulgass  20152  srgpcomp  20153  srgbinom  20166  isdomn2OLD  20645  isdomn3  20648  isorng  20794  lmodvsmmulgdi  20848  cnfldexp  21359  ofldchr  21531  islindf4  21793  assamulgscm  21857  mplcoe1  21992  mplcoe3  21993  mplcoe5  21995  gsummoncoe1  22252  dmatval  22436  dmatel  22437  dmatmulcl  22444  pmatcoe1fsupp  22645  decpmataa0  22712  decpmatmulsumfsupp  22717  pmatcollpw2lem  22721  pm2mpmhmlem1  22762  fiinopn  22845  mretopd  23036  neiptoptop  23075  cnpfval  23178  iscnp3  23188  tgcn  23196  lmbr  23202  lmbr2  23203  lmbrf  23204  lmss  23242  ishaus  23266  hausnei2  23297  t1sep2  23313  fiuncmp  23348  dfconn2  23363  1stcfb  23389  2ndc1stc  23395  1stcrest  23397  1stcelcls  23405  1stccn  23407  lly1stc  23440  elkgen  23480  kgencn  23500  tx1stc  23594  xkopt  23599  cnmptcom  23622  isr0  23681  r0sep  23692  ptcmpfi  23757  isfildlem  23801  rnelfm  23897  fbflim  23920  flimrest  23927  isflf  23937  flffbas  23939  lmflf  23949  fclsrest  23968  isfcf  23978  cnextfvval  24009  tmdgsum  24039  eltsms  24077  tsmsi  24078  tsmsgsum  24083  tsmssubm  24087  tsmsres  24088  tsmsf1o  24089  isust  24148  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  25239  equivcau  25256  caubl  25264  caublcls  25265  ovolgelb  25437  ovolunlem1a  25453  ovolicc2lem3  25476  voliunlem1  25507  voliunlem3  25509  volsuplem  25512  volsup  25513  dyadmax  25555  vitali  25570  itg2leub  25691  itgfsum  25784  dvnadd  25887  dvnres  25889  cpnord  25893  dvnfre  25912  dvmptfsum  25935  dvferm1  25945  dvferm2  25947  rolle  25950  dvlip  25954  c1lip1  25958  lhop1  25975  deg1leb  26056  ply1divex  26098  fta1g  26131  plyco  26202  dgrcolem1  26235  dgrco  26237  dvnply2  26251  plydivex  26261  aalioulem2  26297  aalioulem3  26298  aalioulem5  26300  aaliou3lem2  26307  dvntaylp  26335  taylthlem1  26337  ulmdvlem3  26367  abelthlem9  26406  cxpmul2  26654  scvxcvx  26952  jensenlem2  26954  jensen  26955  wilthlem3  27036  perfectlem2  27197  bcmono  27244  bposlem5  27255  lgsquad2lem2  27352  addsq2reu  27407  2sqreulem1  27413  2sqreunnlem1  27416  dchrisumlem1  27456  dchrisum0flb  27477  pntpbnd1  27553  pntlemf  27572  qabvle  27592  qabvexp  27593  ostthlem2  27595  ostth2lem2  27601  nosupcbv  27670  nosupno  27671  nosupdm  27672  nosupfv  27674  nosupres  27675  nosupbnd1lem1  27676  nosupbnd1lem3  27678  nosupbnd1lem5  27680  noinfcbv  27685  noinfno  27686  noinfdm  27687  noinffv  27689  noinfres  27690  noinfbnd1lem3  27693  noinfbnd1lem5  27695  eqcuts2  27782  addsproplem1  27965  addsprop  27972  negsunif  28051  mulsproplem9  28120  sltmuls2  28144  precsexlem8  28210  precsexlem9  28211  precsexlem11  28213  noseqind  28288  om2noseqrdg  28300  noseqrdgfn  28302  n0addscl  28340  n0mulscl  28341  eucliddivs  28372  peano5uzs  28400  expscllem  28426  expadds  28431  expsne0  28432  expsgt0  28433  pw2cut  28456  pw2cut2  28458  bdaypw2n0bnd  28460  tgcgr4  28603  usgr2pth  29837  wlkiswwlks2lem4  29945  wlkiswwlks2  29948  rusgrnumwwlk  30051  clwlkclwwlklem2a  30073  clwlkclwwlklem1  30074  clwlkclwwlkfo  30084  eupth2  30314  frgr3vlem1  30348  3vfriswmgrlem  30352  3vfriswmgr  30353  wlkl0  30442  numclwlk2lem2f1o  30454  isplig  30551  isnvlem  30685  nvi  30689  nmoubi  30847  nmounbi  30851  nmblolbi  30875  ipasslem1  30906  ipassi  30916  hlim2  31267  pjhth  31468  spansni  31632  elspansn2  31642  pjige0  31766  pjcjt2  31767  pjopyth  31795  elcnop  31932  elcnfn  31957  nmopub  31983  cnopc  31988  nmfnleub  32000  elnlfn  32003  cnfnc  32005  nmbdoplb  32100  nmcexi  32101  nmcoplb  32105  lnfnmul  32123  nmbdfnlb  32125  nmcfnlb  32129  pjss2coi  32239  pjssmi  32240  isst  32288  ishst  32289  stcltr1i  32349  mdbr  32369  dmdbr  32374  mddmd2  32384  mdslmd1lem3  32402  mdslmd1lem4  32403  elat2  32415  atcvat2  32464  cdj1i  32508  iuninc  32635  fmptcof2  32735  nn0min  32901  nexple  32925  wrdt2ind  33035  ismnt  33065  xrge0tsmsd  33155  gsumwun  33158  cyc3genpm  33234  isarchi2  33267  archirng  33270  archiexdiv  33272  archiabl  33280  domnprodn0  33357  islbs5  33461  unitprodclb  33470  mxidlval  33542  1arithidom  33618  1arithufdlem3  33627  crefeq  34002  esumfzf  34226  issiga  34269  isrnsiga  34270  isldsys  34313  ismeas  34356  isrnmeas  34357  measiun  34375  eulerpartlemn  34538  sseqp1  34552  rrvsum  34611  signsply0  34708  signstfvc  34731  bnj941  34928  bnj106  35024  bnj155  35035  bnj590  35066  bnj591  35067  bnj849  35081  bnj893  35084  bnj944  35094  bnj1128  35146  r1filimi  35259  r1omhfb  35268  tz9.1regs  35290  r1omhfbregs  35293  gblacfnacd  35296  subfacp1lem6  35379  erdszelem8  35392  issconn  35420  cvmliftlem7  35485  cvmliftlem10  35488  cvmlift3lem2  35514  satfsschain  35558  satfrel  35561  satfdm  35563  satfrnmapom  35564  fmlafvel  35579  satffun  35603  mrsubvrs  35716  mclsssvlem  35756  mclsval  35757  mclsax  35763  mclsind  35764  shftvalg  35926  bccolsum  35933  iprodefisumlem  35934  faclimlem1  35937  rdgprc  35986  sbequbidv  36408  cbvsbdavw  36448  fveleq  36645  regsfromregtr  36668  unblimceq0  36707  bj-ax12  36858  bj-bm1.3ii  37265  rdgeqoa  37575  finxpreclem6  37601  domalom  37609  ralssiun  37612  wl-ax12v2cl  37711  wl-sblimt  37753  wl-sbhbt  37759  wl-2sb6d  37763  wl-mo2df  37775  wl-mo2t  37780  poimirlem2  37823  poimirlem25  37846  poimirlem28  37849  poimirlem31  37852  heicant  37856  mbfresfi  37867  itg2gt0cn  37876  sdclem2  37943  fdc  37946  seqpo  37948  incsequz  37949  mettrifi  37958  prdsbnd2  37996  heiborlem4  38015  bfplem1  38023  iscringd  38199  maxidlval  38240  igenval2  38267  iss2  38537  elrefrels3  38772  ax12eq  39201  ax12el  39202  ax12indalem  39205  ax12inda2ALT  39206  ax12inda  39208  ax12v2-o  39209  riotasvd  39216  isopos  39440  isat3  39567  ishlat1  39612  glbconN  39637  ispsubsp  40005  isldil  40370  isltrn  40379  isdilN  40414  trlval  40422  cdleme27b  40628  cdleme29b  40635  cdleme31sn1  40641  cdleme31sn1c  40648  cdleme40v  40729  cdlemk36  41173  cdlemkid5  41195  cdlemn11pre  41470  dihord2pre  41485  islpolN  41743  hdmapffval  42086  hdmapfval  42087  hdmapval2lem  42091  uzindd  42231  sticksstones1  42400  sticksstones2  42401  sticksstones3  42402  sticksstones8  42407  sticksstones10  42409  sticksstones11  42410  sticksstones12a  42411  sticksstones15  42415  indstrd  42447  unitscyglem3  42451  nnaddcom  42523  nnadddir  42525  nnmulcom  42527  eu6w  42919  ismrc  42943  incssnn0  42953  mzpexpmpt  42987  pell14qrexpclnn0  43108  monotuz  43183  rmxypos  43189  jm2.17a  43202  jm2.17b  43203  rmygeid  43206  jm2.18  43230  jm2.19lem3  43233  jm2.25  43241  jm2.15nn0  43245  jm2.16nn0  43246  wepwsolem  43284  aomclem8  43303  dfac11  43304  pwslnm  43336  lnr2i  43358  hbtlem5  43370  cnsrexpcl  43407  rngunsnply  43411  unielss  43460  onsucf1lem  43511  cantnfresb  43566  onmcl  43573  naddonnn  43637  elmapintrab  43817  elmapintab  43837  cnvcnvintabd  43841  eliunov2  43920  relexpxpnnidm  43944  relexpiidm  43945  relexpss1d  43946  iunrelexpmin1  43949  relexpmulnn  43950  iunrelexpmin2  43953  relexp0a  43957  trclimalb2  43967  clsk3nimkb  44281  ntrclsiso  44308  ntrclskb  44310  ntrneiiso  44332  ntrneix2  44334  ntrneixb  44336  gneispace2  44373  gneispacess2  44387  mnuunid  44518  dvgrat  44553  pm14.122b  44664  relpeq1  45185  relpeq3  45187  trfr  45203  pwclaxpow  45225  prclaxpr  45226  uniclaxun  45227  modelac8prim  45233  permaxpow  45250  permaxpr  45251  permaxun  45252  nregmodel  45258  fnchoice  45274  fiiuncl  45310  ssinc  45331  ssdec  45332  wessf1ornlem  45429  dmrelrnrel  45470  fperiodmullem  45551  monoordxrv  45725  fmul01  45826  fmuldfeq  45829  climsuselem1  45853  climinff  45857  ellimcabssub0  45863  limcleqr  45888  addlimc  45892  0ellimcdiv  45893  limclner  45895  limsupref  45929  limsupub  45948  limsupmnf  45965  limsupre2lem  45968  limsupre2  45969  limsupre2mpt  45974  limsupre3lem  45976  limsupre3  45977  limsupre3mpt  45978  xlimbr  46071  cnrefiisplem  46073  dvnmptdivc  46182  dvnmptconst  46185  dvnmul  46187  iblspltprt  46217  itgspltprt  46223  stoweidlem2  46246  stoweidlem3  46247  stoweidlem17  46261  stoweidlem19  46263  stoweidlem21  46265  stoweidlem26  46270  fourierdlem42  46393  issal  46558  ismea  46695  isome  46738  carageniuncllem1  46765  caratheodorylem1  46770  2reu8i  47359  2reuimp0  47360  funressndmafv2rn  47469  2ffzoeq  47573  smonoord  47617  fargshiftf1  47687  ichnfimlem  47709  paireqne  47757  reupr  47768  reuopreuprim  47772  perfectALTVlem2  47968  grimcnv  48134  pgnbgreunbgrlem1  48359  pgnbgreunbgrlem4  48365  pgnbgreunbgr  48371  lmodvsmdi  48625  dmatALTval  48646  dmatALTbasel  48648  snlindsntor  48717  ldepsnlinc  48754  elbigo2r  48799  elbigolo1  48803  itcovalt2  48923  mof0  49083  isnrm4  49176  iscnrm3r  49193  iscnrm4  49199  lubsscl  49205  glbsscl  49206  ipolubdm  49232  ipoglbdm  49235  setrecseq  49930  setrec2fun  49937  setrec2lem2  49939