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  2468  mojust  2539  mof  2564  eu6lem  2574  2gencl  3485  3gencl  3486  vtocl2gf  3529  vtocl3gf  3530  vtocl2g  3531  vtocl3g  3532  vtocl2ga  3535  vtocl2gaf  3536  vtocl3gaf  3538  vtocl3ga  3540  vtocl4g  3542  vtocl4ga  3543  eqeu  3666  mo2icl  3674  euind  3684  reu7  3692  reuind  3713  sbctt  3812  sbccomlem  3821  reu8nf  3829  sbcnestgfw  4375  sbcnestgf  4380  r19.36zv  4467  dedth2h  4541  dedth3h  4542  dedth4h  4543  reusngf  4633  reuprg0  4661  preq12bg  4811  elint  4910  elintrabg  4918  intab  4935  axrep1  5227  axreplem  5228  axrep2  5229  axrep6g  5237  bm1.3iiOLD  5249  reusv3  5352  swopolem  5550  solin  5567  freq1  5599  frminex  5611  vtoclr  5695  2optocl  5728  3optocl  5729  raliunxp  5796  resieq  5957  iss  6002  cnveqb  6162  reu3op  6258  reuop  6259  dfpo2  6262  preddowncl  6298  fnbrfvb  6892  fvelimab  6914  fvmptss  6962  fmptco  7084  fprg  7110  fnressn  7113  fressnfv  7115  isoselem  7297  ovg  7533  caovcan  7572  caovordig  7573  caovord  7579  tfisi  7811  tfindsg  7813  tfinds2  7816  tfinds3  7817  dfom2  7820  elom  7821  findsg  7849  finds2  7850  resf1extb  7886  f1o2ndf1  8074  poxp  8080  fnse  8085  xpord3inddlem  8106  soseq  8111  fpr3g  8237  frrlem12  8249  fpr2a  8254  wfr3g  8271  smoeq  8292  smores  8294  smogt  8309  tfrlem1  8317  tfr3  8340  oaordi  8483  oeordi  8525  oeoa  8535  oeoe  8537  nnacl  8549  nnmcl  8550  nnecl  8551  nnacom  8555  nnaordi  8556  nnawordi  8559  nnaass  8560  nndi  8561  nnmass  8562  nnmsucr  8563  nnmcom  8564  nnmordi  8569  naddssim  8623  naddoa  8640  2ecoptocl  8757  3ecoptocl  8758  undifixp  8884  xpdom2g  9013  findcard2  9101  unfi  9107  ssfi  9109  fnfi  9114  fodomfi  9224  imafiOLD  9228  fodomfiOLD  9242  finsschain  9271  marypha1lem  9348  marypha1  9349  supeq1  9360  ordiso2  9432  ordtypelem7  9441  wemaplem1  9463  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  12113  nnindd  12177  nnaddcl  12180  nnmulcl  12181  nnne0  12191  peano5uzi  12593  uzind2  12597  nn0indd  12601  zindd  12605  fzindd  12606  uzaddcl  12829  uzwo  12836  indstr  12841  zmax  12870  xmulasslem  13212  xrsupsslem  13234  xrinfmsslem  13235  xrsupss  13236  xrinfmss  13237  flval2  13746  om2uzlti  13885  uzrdgfni  13893  rabssnn0fi  13921  mptnn0fsupp  13932  seqcl2  13955  seqfveq2  13959  seqshft2  13963  monoord  13967  seqsplit  13970  seqcaopr3  13972  seqf1olem2a  13975  seqf1o  13978  seqid2  13983  seqhomo  13984  ser1const  13993  expcllem  14007  expeq0  14027  mulexp  14036  expadd  14039  expmul  14042  expmordi  14102  leexp2r  14109  leexp1a  14110  bernneq  14164  modexp  14173  facdiv  14222  faclbnd  14225  faclbnd4lem4  14231  hashgadd  14312  hashxp  14369  hashmap  14370  hashf1lem2  14391  hashf1  14392  seqcoll  14399  wrdind  14657  wrd2ind  14658  pfxccatin12lem3  14667  cshweqrep  14756  2cshwcshw  14760  relexp0g  14957  relexpsucnnr  14960  relexpsucnnl  14965  relexpcnv  14970  relexpnndm  14976  relexpaddnn  14986  rtrclreclem1  14992  dfrtrclrec2  14993  rtrclreclem2  14994  rtrclreclem4  14996  dfrtrcl2  14997  relexpind  14999  reusq0  15400  rlim  15430  rlim2  15431  rlim0  15443  rlim0lt  15444  rlimi  15448  ello12r  15452  ello1mpt  15456  ello1d  15458  elo12r  15463  lo1o1  15467  o1lo1  15472  lo1res  15494  climshft  15511  o1compt  15522  rlimo1  15552  lo1add  15562  lo1mul  15563  rlimdiv  15581  climub  15597  climserle  15598  caucvgrlem  15608  caurcvgr  15609  iseraltlem2  15618  summolem2a  15650  sumss  15659  fsum2d  15706  fsumabs  15736  fsumrlim  15746  fsumo1  15747  fsumiun  15756  binom  15765  climcndslem1  15784  climcndslem2  15785  cvgrat  15818  clim2prod  15823  prodfn0  15829  prodfrec  15830  ntrivcvgfvn0  15834  prodmolem2a  15869  fprodabs  15909  fprodn0  15914  fprod2d  15916  binomfallfac  15976  bpolycl  15987  bpolydif  15990  fprodefsum  16030  demoivreALT  16138  ruclem8  16174  ruclem9  16175  dvdsle  16249  dvdsfac  16265  divalglem7  16338  bitsinv1  16381  sadcadd  16397  sadadd2  16399  saddisjlem  16403  smuval2  16421  smupvallem  16422  smu01lem  16424  smupval  16427  smueqlem  16429  smumullem  16431  bezoutlem4  16481  dfgcd2  16485  rplpwr  16497  nn0seqcvgd  16509  seq1st  16510  alginv  16514  algcvga  16518  algfx  16519  lcmf  16572  prmind2  16624  prmdvdsexp  16654  prmfac1  16659  reumodprminv  16744  pcmpt  16832  pcfac  16839  prmpwdvds  16844  prmreclem4  16859  vdwlem10  16930  ramval  16948  ramcl  16969  cshwrepswhash1  17042  prmlem1a  17046  imasleval  17474  ismre  17521  mreexexd  17583  lubprop  18291  lublecllem  18293  glbprop  18304  joinlem  18316  meetlem  18330  poslubmo  18344  posglbmo  18345  poslubd  18346  isglbd  18444  lubun  18450  mndind  18765  frmdgsum  18799  mulgnnass  19051  mhmmulg  19057  gsumwrev  19307  gsmsymgrfix  19369  gsmsymgreq  19373  psgnunilem3  19437  sylow1lem1  19539  efginvrel2  19668  efgsrel  19675  efgredlemd  19685  efgredlem  19688  efgred  19689  efgrelexlemb  19691  gsum2dlem2  19912  gsumcom2  19916  ablfac1eulem  20015  pgpfac1lem2  20018  pgpfac1lem5  20022  pgpfac1  20023  pgpfac  20027  isomnd  20064  omndadd  20069  srgmulgass  20164  srgpcomp  20165  srgbinom  20178  isdomn2OLD  20657  isdomn3  20660  isorng  20806  lmodvsmmulgdi  20860  cnfldexp  21371  ofldchr  21543  islindf4  21805  assamulgscm  21869  mplcoe1  22004  mplcoe3  22005  mplcoe5  22007  gsummoncoe1  22264  dmatval  22448  dmatel  22449  dmatmulcl  22456  pmatcoe1fsupp  22657  decpmataa0  22724  decpmatmulsumfsupp  22729  pmatcollpw2lem  22733  pm2mpmhmlem1  22774  fiinopn  22857  mretopd  23048  neiptoptop  23087  cnpfval  23190  iscnp3  23200  tgcn  23208  lmbr  23214  lmbr2  23215  lmbrf  23216  lmss  23254  ishaus  23278  hausnei2  23309  t1sep2  23325  fiuncmp  23360  dfconn2  23375  1stcfb  23401  2ndc1stc  23407  1stcrest  23409  1stcelcls  23417  1stccn  23419  lly1stc  23452  elkgen  23492  kgencn  23512  tx1stc  23606  xkopt  23611  cnmptcom  23634  isr0  23693  r0sep  23704  ptcmpfi  23769  isfildlem  23813  rnelfm  23909  fbflim  23932  flimrest  23939  isflf  23949  flffbas  23951  lmflf  23961  fclsrest  23980  isfcf  23990  cnextfvval  24021  tmdgsum  24051  eltsms  24089  tsmsi  24090  tsmsgsum  24095  tsmssubm  24099  tsmsres  24100  tsmsf1o  24101  isust  24160  isucn  24233  isucn2  24234  ucnima  24236  imasdsf1olem  24329  metss  24464  met1stc  24477  metcnp  24497  metcnpi  24500  metcnpi2  24501  metucn  24527  xrge0tsms  24791  fsumcn  24829  elcncf  24850  cncfi  24855  rescncf  24858  cncfco  24868  caucfil  25251  equivcau  25268  caubl  25276  caublcls  25277  ovolgelb  25449  ovolunlem1a  25465  ovolicc2lem3  25488  voliunlem1  25519  voliunlem3  25521  volsuplem  25524  volsup  25525  dyadmax  25567  vitali  25582  itg2leub  25703  itgfsum  25796  dvnadd  25899  dvnres  25901  cpnord  25905  dvnfre  25924  dvmptfsum  25947  dvferm1  25957  dvferm2  25959  rolle  25962  dvlip  25966  c1lip1  25970  lhop1  25987  deg1leb  26068  ply1divex  26110  fta1g  26143  plyco  26214  dgrcolem1  26247  dgrco  26249  dvnply2  26263  plydivex  26273  aalioulem2  26309  aalioulem3  26310  aalioulem5  26312  aaliou3lem2  26319  dvntaylp  26347  taylthlem1  26349  ulmdvlem3  26379  abelthlem9  26418  cxpmul2  26666  scvxcvx  26964  jensenlem2  26966  jensen  26967  wilthlem3  27048  perfectlem2  27209  bcmono  27256  bposlem5  27267  lgsquad2lem2  27364  addsq2reu  27419  2sqreulem1  27425  2sqreunnlem1  27428  dchrisumlem1  27468  dchrisum0flb  27489  pntpbnd1  27565  pntlemf  27584  qabvle  27604  qabvexp  27605  ostthlem2  27607  ostth2lem2  27613  nosupcbv  27682  nosupno  27683  nosupdm  27684  nosupfv  27686  nosupres  27687  nosupbnd1lem1  27688  nosupbnd1lem3  27690  nosupbnd1lem5  27692  noinfcbv  27697  noinfno  27698  noinfdm  27699  noinffv  27701  noinfres  27702  noinfbnd1lem3  27705  noinfbnd1lem5  27707  eqcuts2  27794  addsproplem1  27977  addsprop  27984  negsunif  28063  mulsproplem9  28132  sltmuls2  28156  precsexlem8  28222  precsexlem9  28223  precsexlem11  28225  noseqind  28300  om2noseqrdg  28312  noseqrdgfn  28314  n0addscl  28352  n0mulscl  28353  eucliddivs  28384  peano5uzs  28412  expscllem  28438  expadds  28443  expsne0  28444  expsgt0  28445  pw2cut  28468  pw2cut2  28470  bdaypw2n0bnd  28472  tgcgr4  28615  usgr2pth  29849  wlkiswwlks2lem4  29957  wlkiswwlks2  29960  rusgrnumwwlk  30063  clwlkclwwlklem2a  30085  clwlkclwwlklem1  30086  clwlkclwwlkfo  30096  eupth2  30326  frgr3vlem1  30360  3vfriswmgrlem  30364  3vfriswmgr  30365  wlkl0  30454  numclwlk2lem2f1o  30466  isplig  30564  isnvlem  30698  nvi  30702  nmoubi  30860  nmounbi  30864  nmblolbi  30888  ipasslem1  30919  ipassi  30929  hlim2  31280  pjhth  31481  spansni  31645  elspansn2  31655  pjige0  31779  pjcjt2  31780  pjopyth  31808  elcnop  31945  elcnfn  31970  nmopub  31996  cnopc  32001  nmfnleub  32013  elnlfn  32016  cnfnc  32018  nmbdoplb  32113  nmcexi  32114  nmcoplb  32118  lnfnmul  32136  nmbdfnlb  32138  nmcfnlb  32142  pjss2coi  32252  pjssmi  32253  isst  32301  ishst  32302  stcltr1i  32362  mdbr  32382  dmdbr  32387  mddmd2  32397  mdslmd1lem3  32415  mdslmd1lem4  32416  elat2  32428  atcvat2  32477  cdj1i  32521  iuninc  32647  fmptcof2  32747  nn0min  32912  nexple  32936  wrdt2ind  33046  ismnt  33076  xrge0tsmsd  33167  gsumwun  33170  cyc3genpm  33246  isarchi2  33279  archirng  33282  archiexdiv  33284  archiabl  33292  domnprodn0  33369  islbs5  33473  unitprodclb  33482  mxidlval  33554  1arithidom  33630  1arithufdlem3  33639  crefeq  34023  esumfzf  34247  issiga  34290  isrnsiga  34291  isldsys  34334  ismeas  34377  isrnmeas  34378  measiun  34396  eulerpartlemn  34559  sseqp1  34573  rrvsum  34632  signsply0  34729  signstfvc  34752  bnj941  34949  bnj106  35044  bnj155  35055  bnj590  35086  bnj591  35087  bnj849  35101  bnj893  35104  bnj944  35114  bnj1128  35166  r1filimi  35280  r1omhfb  35290  tz9.1regs  35312  r1omhfbregs  35315  gblacfnacd  35318  subfacp1lem6  35401  erdszelem8  35414  issconn  35442  cvmliftlem7  35507  cvmliftlem10  35510  cvmlift3lem2  35536  satfsschain  35580  satfrel  35583  satfdm  35585  satfrnmapom  35586  fmlafvel  35601  satffun  35625  mrsubvrs  35738  mclsssvlem  35778  mclsval  35779  mclsax  35785  mclsind  35786  shftvalg  35948  bccolsum  35955  iprodefisumlem  35956  faclimlem1  35959  rdgprc  36008  sbequbidv  36430  cbvsbdavw  36470  fveleq  36667  regsfromregtr  36690  unblimceq0  36729  bj-ax12  36902  bj-bm1.3ii  37312  rdgeqoa  37625  finxpreclem6  37651  domalom  37659  ralssiun  37662  wl-ax12v2cl  37761  wl-sblimt  37803  wl-sbhbt  37809  wl-2sb6d  37813  wl-mo2df  37825  wl-mo2t  37830  poimirlem2  37873  poimirlem25  37896  poimirlem28  37899  poimirlem31  37902  heicant  37906  mbfresfi  37917  itg2gt0cn  37926  sdclem2  37993  fdc  37996  seqpo  37998  incsequz  37999  mettrifi  38008  prdsbnd2  38046  heiborlem4  38065  bfplem1  38073  iscringd  38249  maxidlval  38290  igenval2  38317  iss2  38595  elrefrels3  38850  ax12eq  39317  ax12el  39318  ax12indalem  39321  ax12inda2ALT  39322  ax12inda  39324  ax12v2-o  39325  riotasvd  39332  isopos  39556  isat3  39683  ishlat1  39728  glbconN  39753  ispsubsp  40121  isldil  40486  isltrn  40495  isdilN  40530  trlval  40538  cdleme27b  40744  cdleme29b  40751  cdleme31sn1  40757  cdleme31sn1c  40764  cdleme40v  40845  cdlemk36  41289  cdlemkid5  41311  cdlemn11pre  41586  dihord2pre  41601  islpolN  41859  hdmapffval  42202  hdmapfval  42203  hdmapval2lem  42207  uzindd  42347  sticksstones1  42516  sticksstones2  42517  sticksstones3  42518  sticksstones8  42523  sticksstones10  42525  sticksstones11  42526  sticksstones12a  42527  sticksstones15  42531  indstrd  42563  unitscyglem3  42567  nnaddcom  42638  nnadddir  42640  nnmulcom  42642  eu6w  43034  ismrc  43058  incssnn0  43068  mzpexpmpt  43102  pell14qrexpclnn0  43223  monotuz  43298  rmxypos  43304  jm2.17a  43317  jm2.17b  43318  rmygeid  43321  jm2.18  43345  jm2.19lem3  43348  jm2.25  43356  jm2.15nn0  43360  jm2.16nn0  43361  wepwsolem  43399  aomclem8  43418  dfac11  43419  pwslnm  43451  lnr2i  43473  hbtlem5  43485  cnsrexpcl  43522  rngunsnply  43526  unielss  43575  onsucf1lem  43626  cantnfresb  43681  onmcl  43688  naddonnn  43752  elmapintrab  43932  elmapintab  43952  cnvcnvintabd  43956  eliunov2  44035  relexpxpnnidm  44059  relexpiidm  44060  relexpss1d  44061  iunrelexpmin1  44064  relexpmulnn  44065  iunrelexpmin2  44068  relexp0a  44072  trclimalb2  44082  clsk3nimkb  44396  ntrclsiso  44423  ntrclskb  44425  ntrneiiso  44447  ntrneix2  44449  ntrneixb  44451  gneispace2  44488  gneispacess2  44502  mnuunid  44633  dvgrat  44668  pm14.122b  44779  relpeq1  45300  relpeq3  45302  trfr  45318  pwclaxpow  45340  prclaxpr  45341  uniclaxun  45342  modelac8prim  45348  permaxpow  45365  permaxpr  45366  permaxun  45367  nregmodel  45373  fnchoice  45389  fiiuncl  45425  ssinc  45446  ssdec  45447  wessf1ornlem  45544  dmrelrnrel  45584  fperiodmullem  45665  monoordxrv  45839  fmul01  45940  fmuldfeq  45943  climsuselem1  45967  climinff  45971  ellimcabssub0  45977  limcleqr  46002  addlimc  46006  0ellimcdiv  46007  limclner  46009  limsupref  46043  limsupub  46062  limsupmnf  46079  limsupre2lem  46082  limsupre2  46083  limsupre2mpt  46088  limsupre3lem  46090  limsupre3  46091  limsupre3mpt  46092  xlimbr  46185  cnrefiisplem  46187  dvnmptdivc  46296  dvnmptconst  46299  dvnmul  46301  iblspltprt  46331  itgspltprt  46337  stoweidlem2  46360  stoweidlem3  46361  stoweidlem17  46375  stoweidlem19  46377  stoweidlem21  46379  stoweidlem26  46384  fourierdlem42  46507  issal  46672  ismea  46809  isome  46852  carageniuncllem1  46879  caratheodorylem1  46884  2reu8i  47473  2reuimp0  47474  funressndmafv2rn  47583  2ffzoeq  47687  smonoord  47731  fargshiftf1  47801  ichnfimlem  47823  paireqne  47871  reupr  47882  reuopreuprim  47886  perfectALTVlem2  48082  grimcnv  48248  pgnbgreunbgrlem1  48473  pgnbgreunbgrlem4  48479  pgnbgreunbgr  48485  lmodvsmdi  48739  dmatALTval  48760  dmatALTbasel  48762  snlindsntor  48831  ldepsnlinc  48868  elbigo2r  48913  elbigolo1  48917  itcovalt2  49037  mof0  49197  isnrm4  49290  iscnrm3r  49307  iscnrm4  49313  lubsscl  49319  glbsscl  49320  ipolubdm  49346  ipoglbdm  49349  setrecseq  50044  setrec2fun  50051  setrec2lem2  50053