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  3473  3gencl  3474  vtocl2gf  3516  vtocl3gf  3517  vtocl2g  3518  vtocl3g  3519  vtocl2ga  3522  vtocl2gaf  3523  vtocl3gaf  3525  vtocl3ga  3527  vtocl4g  3529  vtocl4ga  3530  eqeu  3653  mo2icl  3661  euind  3671  reu7  3679  reuind  3700  sbctt  3799  sbccomlem  3808  reu8nf  3816  sbcnestgfw  4362  sbcnestgf  4367  r19.36zv  4453  dedth2h  4527  dedth3h  4528  dedth4h  4529  reusngf  4619  reuprg0  4647  preq12bg  4797  elint  4896  elintrabg  4904  intab  4921  axrep1  5213  axreplem  5214  axrep2  5215  axrep6g  5225  bm1.3iiOLD  5237  reusv3  5342  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  6954  fmptco  7076  fprg  7102  fnressn  7105  fressnfv  7107  isoselem  7289  ovg  7525  caovcan  7564  caovordig  7565  caovord  7571  tfisi  7803  tfindsg  7805  tfinds2  7808  tfinds3  7809  dfom2  7812  elom  7813  findsg  7841  finds2  7842  resf1extb  7878  f1o2ndf1  8065  poxp  8071  fnse  8076  xpord3inddlem  8097  soseq  8102  fpr3g  8228  frrlem12  8240  fpr2a  8245  wfr3g  8262  smoeq  8283  smores  8285  smogt  8300  tfrlem1  8308  tfr3  8331  oaordi  8474  oeordi  8516  oeoa  8526  oeoe  8528  nnacl  8540  nnmcl  8541  nnecl  8542  nnacom  8546  nnaordi  8547  nnawordi  8550  nnaass  8551  nndi  8552  nnmass  8553  nnmsucr  8554  nnmcom  8555  nnmordi  8560  naddssim  8614  naddoa  8631  2ecoptocl  8748  3ecoptocl  8749  undifixp  8875  xpdom2g  9004  findcard2  9092  unfi  9098  ssfi  9100  fnfi  9105  fodomfi  9215  imafiOLD  9219  fodomfiOLD  9233  finsschain  9262  marypha1lem  9339  marypha1  9340  supeq1  9351  ordiso2  9423  ordtypelem7  9432  wemaplem1  9454  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  20680  isdomn3  20683  isorng  20829  lmodvsmmulgdi  20883  cnfldexp  21394  ofldchr  21566  islindf4  21828  assamulgscm  21891  mplcoe1  22025  mplcoe3  22026  mplcoe5  22028  gsummoncoe1  22283  dmatval  22467  dmatel  22468  dmatmulcl  22475  pmatcoe1fsupp  22676  decpmataa0  22743  decpmatmulsumfsupp  22748  pmatcollpw2lem  22752  pm2mpmhmlem1  22793  fiinopn  22876  mretopd  23067  neiptoptop  23106  cnpfval  23209  iscnp3  23219  tgcn  23227  lmbr  23233  lmbr2  23234  lmbrf  23235  lmss  23273  ishaus  23297  hausnei2  23328  t1sep2  23344  fiuncmp  23379  dfconn2  23394  1stcfb  23420  2ndc1stc  23426  1stcrest  23428  1stcelcls  23436  1stccn  23438  lly1stc  23471  elkgen  23511  kgencn  23531  tx1stc  23625  xkopt  23630  cnmptcom  23653  isr0  23712  r0sep  23723  ptcmpfi  23788  isfildlem  23832  rnelfm  23928  fbflim  23951  flimrest  23958  isflf  23968  flffbas  23970  lmflf  23980  fclsrest  23999  isfcf  24009  cnextfvval  24040  tmdgsum  24070  eltsms  24108  tsmsi  24109  tsmsgsum  24114  tsmssubm  24118  tsmsres  24119  tsmsf1o  24120  isust  24179  isucn  24252  isucn2  24253  ucnima  24255  imasdsf1olem  24348  metss  24483  met1stc  24496  metcnp  24516  metcnpi  24519  metcnpi2  24520  metucn  24546  xrge0tsms  24810  fsumcn  24847  elcncf  24866  cncfi  24871  rescncf  24874  cncfco  24884  caucfil  25260  equivcau  25277  caubl  25285  caublcls  25286  ovolgelb  25457  ovolunlem1a  25473  ovolicc2lem3  25496  voliunlem1  25527  voliunlem3  25529  volsuplem  25532  volsup  25533  dyadmax  25575  vitali  25590  itg2leub  25711  itgfsum  25804  dvnadd  25906  dvnres  25908  cpnord  25912  dvnfre  25929  dvmptfsum  25952  dvferm1  25962  dvferm2  25964  rolle  25967  dvlip  25970  c1lip1  25974  lhop1  25991  deg1leb  26070  ply1divex  26112  fta1g  26145  plyco  26216  dgrcolem1  26248  dgrco  26250  dvnply2  26264  plydivex  26274  aalioulem2  26310  aalioulem3  26311  aalioulem5  26313  aaliou3lem2  26320  dvntaylp  26348  taylthlem1  26350  ulmdvlem3  26380  abelthlem9  26418  cxpmul2  26666  scvxcvx  26963  jensenlem2  26965  jensen  26966  wilthlem3  27047  perfectlem2  27207  bcmono  27254  bposlem5  27265  lgsquad2lem2  27362  addsq2reu  27417  2sqreulem1  27423  2sqreunnlem1  27426  dchrisumlem1  27466  dchrisum0flb  27487  pntpbnd1  27563  pntlemf  27582  qabvle  27602  qabvexp  27603  ostthlem2  27605  ostth2lem2  27611  nosupcbv  27680  nosupno  27681  nosupdm  27682  nosupfv  27684  nosupres  27685  nosupbnd1lem1  27686  nosupbnd1lem3  27688  nosupbnd1lem5  27690  noinfcbv  27695  noinfno  27696  noinfdm  27697  noinffv  27699  noinfres  27700  noinfbnd1lem3  27703  noinfbnd1lem5  27705  eqcuts2  27792  addsproplem1  27975  addsprop  27982  negsunif  28061  mulsproplem9  28130  sltmuls2  28154  precsexlem8  28220  precsexlem9  28221  precsexlem11  28223  noseqind  28298  om2noseqrdg  28310  noseqrdgfn  28312  n0addscl  28350  n0mulscl  28351  eucliddivs  28382  peano5uzs  28410  expscllem  28436  expadds  28441  expsne0  28442  expsgt0  28443  pw2cut  28466  pw2cut2  28468  bdaypw2n0bnd  28470  tgcgr4  28613  usgr2pth  29847  wlkiswwlks2lem4  29955  wlkiswwlks2  29958  rusgrnumwwlk  30061  clwlkclwwlklem2a  30083  clwlkclwwlklem1  30084  clwlkclwwlkfo  30094  eupth2  30324  frgr3vlem1  30358  3vfriswmgrlem  30362  3vfriswmgr  30363  wlkl0  30452  numclwlk2lem2f1o  30464  isplig  30562  isnvlem  30696  nvi  30700  nmoubi  30858  nmounbi  30862  nmblolbi  30886  ipasslem1  30917  ipassi  30927  hlim2  31278  pjhth  31479  spansni  31643  elspansn2  31653  pjige0  31777  pjcjt2  31778  pjopyth  31806  elcnop  31943  elcnfn  31968  nmopub  31994  cnopc  31999  nmfnleub  32011  elnlfn  32014  cnfnc  32016  nmbdoplb  32111  nmcexi  32112  nmcoplb  32116  lnfnmul  32134  nmbdfnlb  32136  nmcfnlb  32140  pjss2coi  32250  pjssmi  32251  isst  32299  ishst  32300  stcltr1i  32360  mdbr  32380  dmdbr  32385  mddmd2  32395  mdslmd1lem3  32413  mdslmd1lem4  32414  elat2  32426  atcvat2  32475  cdj1i  32519  iuninc  32645  fmptcof2  32745  nn0min  32909  nexple  32932  wrdt2ind  33028  ismnt  33058  xrge0tsmsd  33149  gsumwun  33152  cyc3genpm  33228  isarchi2  33261  archirng  33264  archiexdiv  33266  archiabl  33274  domnprodn0  33351  islbs5  33455  unitprodclb  33464  mxidlval  33536  1arithidom  33612  1arithufdlem3  33621  crefeq  34005  esumfzf  34229  issiga  34272  isrnsiga  34273  isldsys  34316  ismeas  34359  isrnmeas  34360  measiun  34378  eulerpartlemn  34541  sseqp1  34555  rrvsum  34614  signsply0  34711  signstfvc  34734  bnj941  34931  bnj106  35026  bnj155  35037  bnj590  35068  bnj591  35069  bnj849  35083  bnj893  35086  bnj944  35096  bnj1128  35148  r1filimi  35262  r1omhfb  35272  tz9.1regs  35294  r1omhfbregs  35297  gblacfnacd  35300  subfacp1lem6  35383  erdszelem8  35396  issconn  35424  cvmliftlem7  35489  cvmliftlem10  35492  cvmlift3lem2  35518  satfsschain  35562  satfrel  35565  satfdm  35567  satfrnmapom  35568  fmlafvel  35583  satffun  35607  mrsubvrs  35720  mclsssvlem  35760  mclsval  35761  mclsax  35767  mclsind  35768  shftvalg  35930  bccolsum  35937  iprodefisumlem  35938  faclimlem1  35941  rdgprc  35990  sbequbidv  36412  cbvsbdavw  36452  fveleq  36649  dfttc4lem1  36726  dfttc4  36728  elttcirr  36729  regsfromregtco  36736  mh-unprimbi  36742  unblimceq0  36783  bj-ax12  36967  bj-bm1.3ii  37387  rdgeqoa  37700  finxpreclem6  37726  domalom  37734  ralssiun  37737  wl-ax12v2cl  37836  wl-sblimt  37887  wl-sbhbt  37893  wl-2sb6d  37897  wl-mo2df  37909  wl-mo2t  37914  poimirlem2  37957  poimirlem25  37980  poimirlem28  37983  poimirlem31  37986  heicant  37990  mbfresfi  38001  itg2gt0cn  38010  sdclem2  38077  fdc  38080  seqpo  38082  incsequz  38083  mettrifi  38092  prdsbnd2  38130  heiborlem4  38149  bfplem1  38157  iscringd  38333  maxidlval  38374  igenval2  38401  iss2  38679  elrefrels3  38934  ax12eq  39401  ax12el  39402  ax12indalem  39405  ax12inda2ALT  39406  ax12inda  39408  ax12v2-o  39409  riotasvd  39416  isopos  39640  isat3  39767  ishlat1  39812  glbconN  39837  ispsubsp  40205  isldil  40570  isltrn  40579  isdilN  40614  trlval  40622  cdleme27b  40828  cdleme29b  40835  cdleme31sn1  40841  cdleme31sn1c  40848  cdleme40v  40929  cdlemk36  41373  cdlemkid5  41395  cdlemn11pre  41670  dihord2pre  41685  islpolN  41943  hdmapffval  42286  hdmapfval  42287  hdmapval2lem  42291  uzindd  42431  sticksstones1  42599  sticksstones2  42600  sticksstones3  42601  sticksstones8  42606  sticksstones10  42608  sticksstones11  42609  sticksstones12a  42610  sticksstones15  42614  indstrd  42646  unitscyglem3  42650  eu6w  43123  ismrc  43147  incssnn0  43157  mzpexpmpt  43191  pell14qrexpclnn0  43312  monotuz  43387  rmxypos  43393  jm2.17a  43406  jm2.17b  43407  rmygeid  43410  jm2.18  43434  jm2.19lem3  43437  jm2.25  43445  jm2.15nn0  43449  jm2.16nn0  43450  wepwsolem  43488  aomclem8  43507  dfac11  43508  pwslnm  43540  lnr2i  43562  hbtlem5  43574  cnsrexpcl  43611  rngunsnply  43615  unielss  43664  onsucf1lem  43715  cantnfresb  43770  onmcl  43777  naddonnn  43841  elmapintrab  44021  elmapintab  44041  cnvcnvintabd  44045  eliunov2  44124  relexpxpnnidm  44148  relexpiidm  44149  relexpss1d  44150  iunrelexpmin1  44153  relexpmulnn  44154  iunrelexpmin2  44157  relexp0a  44161  trclimalb2  44171  clsk3nimkb  44485  ntrclsiso  44512  ntrclskb  44514  ntrneiiso  44536  ntrneix2  44538  ntrneixb  44540  gneispace2  44577  gneispacess2  44591  mnuunid  44722  dvgrat  44757  pm14.122b  44868  relpeq1  45389  relpeq3  45391  trfr  45407  pwclaxpow  45429  prclaxpr  45430  uniclaxun  45431  modelac8prim  45437  permaxpow  45454  permaxpr  45455  permaxun  45456  nregmodel  45462  fnchoice  45478  fiiuncl  45514  ssinc  45535  ssdec  45536  wessf1ornlem  45633  dmrelrnrel  45673  fperiodmullem  45754  monoordxrv  45927  fmul01  46028  fmuldfeq  46031  climsuselem1  46055  climinff  46059  ellimcabssub0  46065  limcleqr  46090  addlimc  46094  0ellimcdiv  46095  limclner  46097  limsupref  46131  limsupub  46150  limsupmnf  46167  limsupre2lem  46170  limsupre2  46171  limsupre2mpt  46176  limsupre3lem  46178  limsupre3  46179  limsupre3mpt  46180  xlimbr  46273  cnrefiisplem  46275  dvnmptdivc  46384  dvnmptconst  46387  dvnmul  46389  iblspltprt  46419  itgspltprt  46425  stoweidlem2  46448  stoweidlem3  46449  stoweidlem17  46463  stoweidlem19  46465  stoweidlem21  46467  stoweidlem26  46472  fourierdlem42  46595  issal  46760  ismea  46897  isome  46940  carageniuncllem1  46967  caratheodorylem1  46972  2reu8i  47573  2reuimp0  47574  funressndmafv2rn  47683  2ffzoeq  47788  smonoord  47837  fargshiftf1  47913  ichnfimlem  47935  paireqne  47983  reupr  47994  reuopreuprim  47998  perfectALTVlem2  48210  grimcnv  48376  pgnbgreunbgrlem1  48601  pgnbgreunbgrlem4  48607  pgnbgreunbgr  48613  lmodvsmdi  48867  dmatALTval  48888  dmatALTbasel  48890  snlindsntor  48959  ldepsnlinc  48996  elbigo2r  49041  elbigolo1  49045  itcovalt2  49165  mof0  49325  isnrm4  49418  iscnrm3r  49435  iscnrm4  49441  lubsscl  49447  glbsscl  49448  ipolubdm  49474  ipoglbdm  49477  setrecseq  50172  setrec2fun  50179  setrec2lem2  50181