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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  imbi12d  345  imbi2  349  pm5.42  544  orbi2d  913  19.23t  2207  axc14  2465  mojust  2541  mof  2565  eu6lem  2575  nfabdwOLD  2933  2gencl  3471  3gencl  3472  vtocl2gf  3507  vtocl3gf  3508  vtocl2g  3509  vtocl3g  3510  vtocl2ga  3513  vtocl4g  3518  eqeu  3645  mo2icl  3653  euind  3663  reu7  3671  reuind  3692  sbctt  3797  reu8nf  3815  sbcnestgfw  4358  sbcnestgf  4363  r19.36zv  4443  dedth2h  4524  dedth3h  4525  dedth4h  4526  reusngf  4614  reuprg0  4644  preq12bg  4790  elint  4891  elintrabg  4898  intab  4915  axrep1  5215  axreplem  5216  axrep2  5217  bm1.3ii  5230  reusv3  5332  poclOLD  5511  swopolem  5513  solin  5528  freq1  5559  frminex  5569  vtoclr  5650  2optocl  5681  3optocl  5682  raliunxp  5746  resieq  5900  iss  5941  cnveqb  6097  reu3op  6193  reuop  6194  dfpo2  6197  preddowncl  6233  funmo  6447  funimaexg  6517  fnbrfvb  6817  fvelimab  6836  fvmptss  6882  fmptco  6996  fprg  7022  fnressn  7025  fressnfv  7027  isoselem  7206  ovg  7429  caovcan  7468  caovordig  7469  caovord  7475  tfisi  7697  tfindsg  7699  tfinds2  7702  tfinds3  7703  dfom2  7706  elom  7707  findsg  7738  finds2  7739  f1o2ndf1  7952  poxp  7958  fnse  7963  fpr3g  8090  frrlem12  8102  fpr2a  8107  wfr3g  8127  wfrlem4OLD  8132  smoeq  8170  smores  8172  smogt  8187  tfrlem1  8196  tfr3  8219  oaordi  8360  oeordi  8401  oeoa  8411  oeoe  8413  nnacl  8425  nnmcl  8426  nnecl  8427  nnacom  8431  nnaordi  8432  nnawordi  8435  nnaass  8436  nndi  8437  nnmass  8438  nnmsucr  8439  nnmcom  8440  nnmordi  8445  2ecoptocl  8578  3ecoptocl  8579  undifixp  8703  xpdom2g  8835  findcard2  8927  unfi  8935  ssfi  8936  imafi  8938  fnfi  8944  findcard2OLD  9032  xpfi  9061  fodomfi  9068  finsschain  9102  marypha1lem  9168  marypha1  9169  supeq1  9180  ordiso2  9250  ordtypelem7  9259  wemaplem1  9281  inf3lem2  9363  inf3lem5  9366  infdiffi  9392  cantnfval2  9403  cantnfle  9405  cantnfp1lem3  9414  oemapval  9417  cantnflem1  9423  cantnf  9427  wemapwe  9431  cnfcom  9434  cnfcom3clem  9439  ttrclss  9454  ttrclselem2  9460  trpredmintr  9476  tz9.1  9485  frminOLD  9506  frr3g  9513  frr2  9517  r1pwALT  9603  cplem2  9647  karden  9652  updjud  9691  infxpenc2lem2  9775  fseqenlem1  9779  dfac8clem  9787  alephinit  9850  dfac4  9877  dfac5lem5  9882  dfac2a  9884  dfac2b  9885  dfacacn  9896  dfac12lem3  9900  kmlem2  9906  kmlem13  9917  nnadju  9952  ackbij1lem16  9990  sornom  10032  infpssrlem4  10061  fin23lem14  10088  fin23lem32  10099  fin23lem34  10101  fin23lem36  10103  isf32lem1  10108  isf32lem2  10109  axcc2lem  10191  axcc3  10193  axcclem  10212  zornn0g  10260  ttukeylem5  10268  ttukeylem6  10269  axrepnd  10349  axpowndlem3  10354  zfcndrep  10369  fpwwe2lem7  10392  pwfseqlem3  10415  wunr1om  10474  wunfi  10476  tskr1om  10522  ingru  10570  grudomon  10572  axgroth3  10586  axgroth4  10587  nqereu  10684  mulcanenq  10715  elnp  10742  elnpi  10743  prlem934  10788  infm3  11932  nnindd  11991  nnaddcl  11994  nnmulcl  11995  nnne0  12005  peano5uzi  12407  uzind2  12411  nn0indd  12415  zindd  12419  eluzadd  12610  uzaddcl  12641  uzwo  12648  indstr  12653  zmax  12682  xmulasslem  13016  xrsupsslem  13038  xrinfmsslem  13039  xrsupss  13040  xrinfmss  13041  flval2  13530  om2uzlti  13666  uzrdgfni  13674  rabssnn0fi  13702  mptnn0fsupp  13713  seqcl2  13737  seqfveq2  13741  seqshft2  13745  monoord  13749  seqsplit  13752  seqcaopr3  13754  seqf1olem2a  13757  seqf1o  13760  seqid2  13765  seqhomo  13766  ser1const  13775  expcllem  13789  expeq0  13809  mulexp  13818  expadd  13821  expmul  13824  expmordi  13881  leexp2r  13888  leexp1a  13889  bernneq  13940  modexp  13949  facdiv  13997  faclbnd  14000  faclbnd4lem4  14006  hashgadd  14088  hashxp  14145  hashmap  14146  hashf1lem2  14166  hashf1  14167  seqcoll  14174  wrdind  14431  wrd2ind  14432  pfxccatin12lem3  14441  cshweqrep  14530  2cshwcshw  14534  relexp0g  14729  relexpsucnnr  14732  relexpsucnnl  14737  relexpcnv  14742  relexpnndm  14748  relexpaddnn  14758  rtrclreclem1  14764  dfrtrclrec2  14765  rtrclreclem2  14766  rtrclreclem4  14768  dfrtrcl2  14769  relexpind  14771  reusq0  15170  rlim  15200  rlim2  15201  rlim0  15213  rlim0lt  15214  rlimi  15218  ello12r  15222  ello1mpt  15226  ello1d  15228  elo12r  15233  lo1o1  15237  o1lo1  15242  lo1res  15264  climshft  15281  o1compt  15292  rlimo1  15322  lo1add  15332  lo1mul  15333  rlimdiv  15353  climub  15369  climserle  15370  caucvgrlem  15380  caurcvgr  15381  iseraltlem2  15390  summolem2a  15423  sumss  15432  fsum2d  15479  fsumabs  15509  fsumrlim  15519  fsumo1  15520  fsumiun  15529  binom  15538  climcndslem1  15557  climcndslem2  15558  cvgrat  15591  clim2prod  15596  prodfn0  15602  prodfrec  15603  ntrivcvgfvn0  15607  prodmolem2a  15640  fprodabs  15680  fprodn0  15685  fprod2d  15687  binomfallfac  15747  bpolycl  15758  bpolydif  15761  fprodefsum  15800  demoivreALT  15906  ruclem8  15942  ruclem9  15943  dvdsle  16015  dvdsfac  16031  divalglem7  16104  bitsinv1  16145  sadcadd  16161  sadadd2  16163  saddisjlem  16167  smuval2  16185  smupvallem  16186  smu01lem  16188  smupval  16191  smueqlem  16193  smumullem  16195  bezoutlem4  16246  dfgcd2  16250  gcdmultipleOLD  16256  rplpwr  16263  nn0seqcvgd  16271  seq1st  16272  alginv  16276  algcvga  16280  algfx  16281  lcmf  16334  prmind2  16386  prmdvdsexp  16416  prmfac1  16422  reumodprminv  16501  pcmpt  16589  pcfac  16596  prmpwdvds  16601  prmreclem4  16616  vdwlem10  16687  ramval  16705  ramcl  16726  cshwrepswhash1  16800  prmlem1a  16804  imasleval  17248  ismre  17295  mreexexd  17353  lubprop  18072  lublecllem  18074  glbprop  18085  joinlem  18097  meetlem  18111  poslubmo  18125  posglbmo  18126  poslubd  18127  isglbd  18223  lubun  18229  mndind  18462  frmdgsum  18497  mulgnnass  18734  mhmmulg  18740  gsumwrev  18969  gsmsymgrfix  19032  gsmsymgreq  19036  psgnunilem3  19100  sylow1lem1  19199  efginvrel2  19329  efgsrel  19336  efgredlemd  19346  efgredlem  19349  efgred  19350  efgrelexlemb  19352  gsum2dlem2  19568  gsumcom2  19572  ablfac1eulem  19671  pgpfac1lem2  19674  pgpfac1lem5  19678  pgpfac1  19679  pgpfac  19683  srgmulgass  19763  srgpcomp  19764  srgbinom  19777  lmodvsmmulgdi  20154  isdomn2  20566  cnfldexp  20627  islindf4  21041  assamulgscm  21101  mplcoe1  21234  mplcoe3  21235  mplcoe5  21237  gsummoncoe1  21471  dmatval  21637  dmatel  21638  dmatmulcl  21645  pmatcoe1fsupp  21846  decpmataa0  21913  decpmatmulsumfsupp  21918  pmatcollpw2lem  21922  pm2mpmhmlem1  21963  fiinopn  22046  mretopd  22239  neiptoptop  22278  cnpfval  22381  iscnp3  22391  tgcn  22399  lmbr  22405  lmbr2  22406  lmbrf  22407  lmss  22445  ishaus  22469  hausnei2  22500  t1sep2  22516  fiuncmp  22551  dfconn2  22566  1stcfb  22592  2ndc1stc  22598  1stcrest  22600  1stcelcls  22608  1stccn  22610  lly1stc  22643  elkgen  22683  kgencn  22703  tx1stc  22797  xkopt  22802  cnmptcom  22825  isr0  22884  r0sep  22895  ptcmpfi  22960  isfildlem  23004  rnelfm  23100  fbflim  23123  flimrest  23130  isflf  23140  flffbas  23142  lmflf  23152  fclsrest  23171  isfcf  23181  cnextfvval  23212  tmdgsum  23242  eltsms  23280  tsmsi  23281  tsmsgsum  23286  tsmssubm  23290  tsmsres  23291  tsmsf1o  23292  isust  23351  isucn  23426  isucn2  23427  ucnima  23429  imasdsf1olem  23522  metss  23660  met1stc  23673  metcnp  23693  metcnpi  23696  metcnpi2  23697  metucn  23723  xrge0tsms  23993  fsumcn  24029  elcncf  24048  cncfi  24053  rescncf  24056  cncfco  24066  caucfil  24443  equivcau  24460  caubl  24468  caublcls  24469  ovolgelb  24640  ovolunlem1a  24656  ovolicc2lem3  24679  voliunlem1  24710  voliunlem3  24712  volsuplem  24715  volsup  24716  dyadmax  24758  vitali  24773  itg2leub  24895  itgfsum  24987  dvnadd  25089  dvnres  25091  cpnord  25095  dvnfre  25112  dvmptfsum  25135  dvferm1  25145  dvferm2  25147  rolle  25150  dvlip  25153  c1lip1  25157  lhop1  25174  deg1leb  25256  ply1divex  25297  fta1g  25328  plyco  25398  dgrcolem1  25430  dgrco  25432  dvnply2  25443  plydivex  25453  aalioulem2  25489  aalioulem3  25490  aalioulem5  25492  aaliou3lem2  25499  dvntaylp  25526  taylthlem1  25528  ulmdvlem3  25557  abelthlem9  25595  cxpmul2  25840  scvxcvx  26131  jensenlem2  26133  jensen  26134  wilthlem3  26215  perfectlem2  26374  bcmono  26421  bposlem5  26432  lgsquad2lem2  26529  addsq2reu  26584  2sqreulem1  26590  2sqreunnlem1  26593  dchrisumlem1  26633  dchrisum0flb  26654  pntpbnd1  26730  pntlemf  26749  qabvle  26769  qabvexp  26770  ostthlem2  26772  ostth2lem2  26778  tgcgr4  26888  usgr2pth  28126  wlkiswwlks2lem4  28231  wlkiswwlks2  28234  rusgrnumwwlk  28334  clwlkclwwlklem2a  28356  clwlkclwwlklem1  28357  clwlkclwwlkfo  28367  eupth2  28597  frgr3vlem1  28631  3vfriswmgrlem  28635  3vfriswmgr  28636  wlkl0  28725  numclwlk2lem2f1o  28737  isplig  28832  isnvlem  28966  nvi  28970  nmoubi  29128  nmounbi  29132  nmblolbi  29156  ipasslem1  29187  ipassi  29197  hlim2  29548  pjhth  29749  spansni  29913  elspansn2  29923  pjige0  30047  pjcjt2  30048  pjopyth  30076  elcnop  30213  elcnfn  30238  nmopub  30264  cnopc  30269  nmfnleub  30281  elnlfn  30284  cnfnc  30286  nmbdoplb  30381  nmcexi  30382  nmcoplb  30386  lnfnmul  30404  nmbdfnlb  30406  nmcfnlb  30410  pjss2coi  30520  pjssmi  30521  isst  30569  ishst  30570  stcltr1i  30630  mdbr  30650  dmdbr  30655  mddmd2  30665  mdslmd1lem3  30683  mdslmd1lem4  30684  elat2  30696  atcvat2  30745  cdj1i  30789  iuninc  30894  fmptcof2  30988  nn0min  31128  wrdt2ind  31219  ismnt  31255  xrge0tsmsd  31311  isomnd  31321  omndadd  31326  cyc3genpm  31413  isarchi2  31433  archirng  31436  archiexdiv  31438  archiabl  31446  isorng  31492  ofldchr  31507  mxidlval  31627  crefeq  31789  nexple  31971  esumfzf  32031  issiga  32074  isrnsiga  32075  isldsys  32118  ismeas  32161  isrnmeas  32162  measiun  32180  eulerpartlemn  32342  sseqp1  32356  rrvsum  32415  signsply0  32524  signstfvc  32547  bnj941  32746  bnj106  32842  bnj155  32853  bnj590  32884  bnj591  32885  bnj849  32899  bnj893  32902  bnj944  32912  bnj1128  32964  subfacp1lem6  33141  erdszelem8  33154  issconn  33182  cvmliftlem7  33247  cvmliftlem10  33250  cvmlift3lem2  33276  satfsschain  33320  satfrel  33323  satfdm  33325  satfrnmapom  33326  fmlafvel  33341  satffun  33365  mrsubvrs  33478  mclsssvlem  33518  mclsval  33519  mclsax  33525  mclsind  33526  shftvalg  33691  bccolsum  33699  iprodefisumlem  33700  faclimlem1  33703  rdgprc  33764  soseq  33797  naddssim  33831  nosupcbv  33899  nosupno  33900  nosupdm  33901  nosupfv  33903  nosupres  33904  nosupbnd1lem1  33905  nosupbnd1lem3  33907  nosupbnd1lem5  33909  noinfcbv  33914  noinfno  33915  noinfdm  33916  noinffv  33918  noinfres  33919  noinfbnd1lem3  33922  noinfbnd1lem5  33924  eqscut2  33994  fveleq  34634  unblimceq0  34681  bj-ax12  34832  bj-bm1.3ii  35229  rdgeqoa  35535  finxpreclem6  35561  domalom  35569  ralssiun  35572  wl-sblimt  35700  wl-sbhbt  35703  wl-2sb6d  35707  wl-mo2df  35719  wl-mo2t  35724  poimirlem2  35773  poimirlem25  35796  poimirlem28  35799  poimirlem31  35802  heicant  35806  mbfresfi  35817  itg2gt0cn  35826  sdclem2  35894  fdc  35897  seqpo  35899  incsequz  35900  mettrifi  35909  prdsbnd2  35947  heiborlem4  35966  bfplem1  35974  iscringd  36150  maxidlval  36191  igenval2  36218  iss2  36473  elrefrels3  36630  ax12eq  36949  ax12el  36950  ax12indalem  36953  ax12inda2ALT  36954  ax12inda  36956  ax12v2-o  36957  riotasvd  36964  isopos  37188  isat3  37315  ishlat1  37360  glbconN  37385  ispsubsp  37753  isldil  38118  isltrn  38127  isdilN  38162  trlval  38170  cdleme27b  38376  cdleme29b  38383  cdleme31sn1  38389  cdleme31sn1c  38396  cdleme40v  38477  cdlemk36  38921  cdlemkid5  38943  cdlemn11pre  39218  dihord2pre  39233  islpolN  39491  hdmapffval  39834  hdmapfval  39835  hdmapval2lem  39839  fzindd  39979  uzindd  39980  sticksstones1  40097  sticksstones2  40098  sticksstones3  40099  sticksstones8  40104  sticksstones10  40106  sticksstones11  40107  sticksstones12a  40108  sticksstones15  40112  nnaddcom  40293  nnadddir  40295  nnmulcom  40297  ismrc  40518  incssnn0  40528  mzpexpmpt  40562  pell14qrexpclnn0  40683  monotuz  40758  rmxypos  40764  jm2.17a  40777  jm2.17b  40778  rmygeid  40781  jm2.18  40805  jm2.19lem3  40808  jm2.25  40816  jm2.15nn0  40820  jm2.16nn0  40821  wepwsolem  40862  aomclem8  40881  dfac11  40882  pwslnm  40914  lnr2i  40936  hbtlem5  40948  cnsrexpcl  40985  rngunsnply  40993  isdomn3  41024  ifpbi23  41057  elmapintrab  41152  elmapintab  41172  cnvcnvintabd  41176  eliunov2  41255  relexpxpnnidm  41279  relexpiidm  41280  relexpss1d  41281  iunrelexpmin1  41284  relexpmulnn  41285  iunrelexpmin2  41288  relexp0a  41292  trclimalb2  41302  clsk3nimkb  41618  ntrclsiso  41645  ntrclskb  41647  ntrneiiso  41669  ntrneix2  41671  ntrneixb  41673  gneispace2  41710  gneispacess2  41724  mnuunid  41863  dvgrat  41898  pm14.122b  42009  fnchoice  42540  fiiuncl  42581  ssinc  42605  ssdec  42606  wessf1ornlem  42690  dmrelrnrel  42733  fperiodmullem  42811  monoordxrv  42991  fmul01  43090  fmuldfeq  43093  climsuselem1  43117  climinff  43121  ellimcabssub0  43127  limcleqr  43154  addlimc  43158  0ellimcdiv  43159  limclner  43161  limsupref  43195  limsupub  43214  limsupmnf  43231  limsupre2lem  43234  limsupre2  43235  limsupre2mpt  43240  limsupre3lem  43242  limsupre3  43243  limsupre3mpt  43244  xlimbr  43337  cnrefiisplem  43339  dvnmptdivc  43448  dvnmptconst  43451  dvnmul  43453  iblspltprt  43483  itgspltprt  43489  stoweidlem2  43512  stoweidlem3  43513  stoweidlem17  43527  stoweidlem19  43529  stoweidlem21  43531  stoweidlem26  43536  fourierdlem42  43659  issal  43824  ismea  43958  isome  44001  carageniuncllem1  44028  caratheodorylem1  44033  2reu8i  44571  2reuimp0  44572  funressndmafv2rn  44681  2ffzoeq  44787  smonoord  44790  fargshiftf1  44860  ichnfimlem  44882  paireqne  44930  reupr  44941  reuopreuprim  44945  perfectALTVlem2  45141  lmodvsmdi  45685  dmatALTval  45708  dmatALTbasel  45710  snlindsntor  45779  ldepsnlinc  45816  elbigo2r  45866  elbigolo1  45870  itcovalt2  45990  mof0  46132  isnrm4  46191  iscnrm3r  46209  iscnrm4  46215  lubsscl  46221  glbsscl  46222  ipolubdm  46240  ipoglbdm  46243  setrecseq  46358  setrec2fun  46365  setrec2lem2  46367