Theorem imbi2d 343

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 26	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒)))
3	2	pm5.74d 276	1 ⊢ (𝜑 → ((𝜃 → 𝜓) ↔ (𝜃 → 𝜒)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  imbi12d  347  imbi2  351  pm5.42  553  orbi2d  929  19.23t  2250  axc14  2495  mojust  2566  mof  2591  eu6lem  2601  2gencl  3496  3gencl  3497  vtocl2gf  3535  vtocl3gf  3536  vtocl2g  3537  vtocl3g  3538  vtocl2ga  3541  vtocl2gaf  3542  vtocl3gaf  3543  vtocl3ga  3544  vtocl4g  3545  vtocl4ga  3546  eqeu  3667  mo2icl  3675  euind  3685  reu7  3693  reuind  3714  sbctt  3811  sbccomlem  3821  reu8nf  3828  sbcnestgfw  4382  sbcnestgf  4387  r19.36zv  4471  dedth2h  4545  dedth3h  4546  dedth4h  4547  reusngf  4636  reuprg0  4664  preq12bg  4813  elint  4918  elintrabg  4926  intab  4943  axrep1  5239  axreplem  5240  axrep2  5241  axrep6g  5249  reusv3  5374  swopolem  5576  solin  5593  freq1  5625  frminex  5637  vtoclr  5721  2optocl  5755  3optocl  5756  raliunxp  5826  resieq  5997  iss  6045  reu3op  6321  reuop  6322  dfpo2  6325  preddowncl  6361  fnbrfvb  6966  fvelimab  6988  fvmptss  7037  fmptco  7162  fprg  7191  fnressn  7194  fressnfv  7196  isoselem  7380  ovg  7617  caovcan  7657  caovordig  7658  caovord  7664  tfisi  7904  tfindsg  7906  tfinds2  7909  tfinds3  7910  dfom2  7913  elom  7914  findsg  7943  finds2  7944  resf1extb  7980  f1o2ndf1  8170  poxp  8177  fnse  8187  xpord3inddlem  8208  soseq  8213  fpr3g  8341  frrlem12  8353  fpr2a  8358  wfr3g  8375  smoeq  8396  smores  8398  smogt  8413  tfrlem1  8421  tfr3  8445  tz7.48lem  8488  oaordi  8592  oeordi  8634  oeoa  8644  oeoe  8646  nnacl  8658  nnmcl  8659  nnecl  8660  nnacom  8664  nnaordi  8665  nnawordi  8668  nnaass  8669  nndi  8670  nnmass  8671  nnmsucr  8672  nnmcom  8673  nnmordi  8678  naddssim  8733  naddoa  8750  2ecoptocl  8867  3ecoptocl  8868  undifixp  9000  xpdom2g  9130  findcard2  9218  unfi  9224  ssfi  9226  fnfi  9231  fodomfi  9342  finsschain  9386  marypha1lem  9462  marypha1  9463  supeq1  9474  ordiso2  9546  ordtypelem7  9555  wemaplem1  9577  inf3lem2  9667  inf3lem5  9670  infdiffi  9696  cantnfval2  9707  cantnfle  9709  cantnfp1lem3  9718  oemapval  9721  cantnflem1  9727  cantnf  9731  wemapwe  9735  cnfcom  9738  cnfcom3clem  9743  ttrclss  9758  ttrclselem2  9764  tz9.1  9767  frr3g  9797  frr2  9801  r1pwALT  9897  r1filimi  9940  cplem2  9989  cplem2OLD  9990  kardenOLD  9997  setrec2fun  10010  setrec2lem2  10013  updjud  10052  infxpenc2lem2  10138  fseqenlem1  10142  dfac8clem  10150  alephinit  10213  dfac4  10240  dfac5lem5  10245  dfac2a  10247  dfac2b  10248  dfacacn  10259  dfac12lem3  10263  kmlem2  10269  kmlem13  10280  nnadju  10315  ackbij1lem16  10351  sornom  10394  infpssrlem4  10423  fin23lem14  10450  fin23lem32  10461  fin23lem34  10463  fin23lem36  10465  isf32lem1  10470  isf32lem2  10471  axcc2lem  10553  axcc3  10555  axcclem  10574  zornn0g  10622  ttukeylem5  10630  ttukeylem6  10631  axrepnd  10718  axpowndlem3  10723  zfcndrep  10738  fpwwe2lem7  10761  pwfseqlem3  10784  wunr1om  10843  wunfi  10845  tskr1om  10891  ingru  10939  grudomon  10941  axgroth3  10955  axgroth4  10956  nqereu  11053  mulcanenq  11084  elnp  11111  elnpi  11112  prlem934  11157  infm3  12316  nnindd  12395  nnaddcl  12398  nnmulcl  12399  nnaddcom  12402  nnne0  12412  nnadddir  12434  nnmulcom  12436  peano5uzi  12828  uzind2  12832  nn0indd  12836  zindd  12840  fzindd  12841  uzaddcl  13071  uzwo  13078  indstr  13083  zmax  13112  xmulasslem  13455  xrsupsslem  13477  xrinfmsslem  13478  xrsupss  13479  xrinfmss  13480  flval2  13994  om2uzlti  14133  uzrdgfni  14141  rabssnn0fi  14169  mptnn0fsupp  14180  seqcl2  14203  seqfveq2  14207  seqshft2  14211  monoord  14215  seqsplit  14218  seqcaopr3  14220  seqf1olem2a  14223  seqf1o  14226  seqid2  14231  seqhomo  14232  ser1const  14241  expcllem  14255  expeq0  14275  mulexp  14284  expadd  14287  expmul  14290  expmordi  14350  leexp2r  14357  leexp1a  14358  bernneq  14414  modexp  14423  facdiv  14472  faclbnd  14475  faclbnd4lem4  14481  hashgadd  14562  hashxp  14620  hashmap  14621  hashf1lem2  14642  hashf1  14643  seqcoll  14650  wrdind  14913  wrd2ind  14914  pfxccatin12lem3  14923  cshweqrep  15014  2cshwcshw  15018  relexp0g  15218  relexpsucnnr  15221  relexpsucnnl  15226  relexpcnv  15231  relexpnndm  15237  relexpaddnn  15247  rtrclreclem1  15253  dfrtrclrec2  15254  rtrclreclem2  15255  rtrclreclem4  15257  dfrtrcl2  15258  relexpind  15260  reusq0  15676  rlim  15706  rlim2  15707  rlim0  15719  rlim0lt  15720  rlimi  15724  ello12r  15728  ello1mpt  15732  ello1d  15734  elo12r  15739  lo1o1  15743  o1lo1  15748  lo1res  15770  climshft  15787  o1compt  15798  rlimo1  15828  lo1add  15838  lo1mul  15839  rlimdiv  15857  climub  15873  climserle  15874  caucvgrlem  15884  caurcvgr  15885  iseraltlem2  15894  summolem2a  15925  sumss  15934  fsum2d  15981  fsumabs  16012  fsumrlim  16022  fsumo1  16023  fsumiun  16032  binom  16043  climcndslem1  16062  climcndslem2  16063  cvgrat  16096  clim2prod  16101  prodfn0  16107  prodfrec  16108  ntrivcvgfvn0  16112  prodmolem2a  16145  fprodabs  16185  fprodn0  16190  fprod2d  16192  binomfallfac  16251  bpolycl  16262  bpolydif  16265  fprodefsum  16305  demoivreALT  16413  ruclem8  16449  ruclem9  16450  dvdsle  16524  dvdsfac  16540  divalglem7  16613  bitsinv1  16656  sadcadd  16672  sadadd2  16674  saddisjlem  16678  smuval2  16696  smupvallem  16697  smu01lem  16699  smupval  16702  smueqlem  16704  smumullem  16706  bezoutlem4  16759  dfgcd2  16763  rplpwr  16776  nn0seqcvgd  16789  seq1st  16790  alginv  16794  algcvga  16798  algfx  16799  lcmf  16852  prmind2  16904  prmdvdsexp  16935  prmfac1  16940  reumodprminv  17026  pcmpt  17114  pcfac  17121  prmpwdvds  17126  prmreclem4  17141  vdwlem10  17212  ramval  17230  ramcl  17251  cshwrepswhash1  17324  prmlem1a  17328  imasleval  17763  ismre  17810  mreexexd  17872  lubprop  18580  lublecllem  18582  glbprop  18593  joinlem  18605  meetlem  18619  poslubmo  18633  posglbmo  18634  poslubd  18635  isglbd  18733  lubun  18739  mndind  19074  frmdgsum  19108  mulgnnass  19369  mhmmulg  19375  gsumwrev  19631  gsmsymgrfix  19693  gsmsymgreq  19697  psgnunilem3  19761  sylow1lem1  19863  efginvrel2  19992  efgsrel  19999  efgredlemd  20009  efgredlem  20012  efgred  20013  efgrelexlemb  20015  gsum2dlem2  20236  gsumcom2  20240  ablfac1eulem  20339  pgpfac1lem2  20342  pgpfac1lem5  20346  pgpfac1  20347  pgpfac  20351  isomnd  20388  omndadd  20393  srgmulgass  20494  srgpcomp  20495  srgbinom  20508  isdomn3  21017  isorng  21169  lmodvsmmulgdi  21223  rspprop  21575  cnfldexp  21763  cnsrexpcl  21778  ofldchr  21937  islindf4  22199  assamulgscm  22264  mplcoe1  22401  mplcoe3  22402  mplcoe5  22404  gsummoncoe1  22681  dmatval  22862  dmatel  22863  dmatmulcl  22870  pmatcoe1fsupp  23074  decpmataa0  23141  decpmatmulsumfsupp  23146  pmatcollpw2lem  23150  pm2mpmhmlem1  23191  fiinopn  23274  mretopd  23465  neiptoptop  23504  cnpfval  23607  iscnp3  23617  tgcn  23625  lmbr  23631  lmbr2  23632  lmbrf  23633  lmss  23671  ishaus  23695  hausnei2  23726  t1sep2  23742  fiuncmp  23777  dfconn2  23792  1stcfb  23818  2ndc1stc  23824  1stcrest  23826  1stcelcls  23835  1stccn  23837  lly1stc  23870  elkgen  23910  kgencn  23930  tx1stc  24024  xkopt  24029  cnmptcom  24052  isr0  24111  r0sep  24122  ptcmpfi  24187  isfildlem  24231  rnelfm  24327  fbflim  24350  flimrest  24357  isflf  24367  flffbas  24369  lmflf  24379  fclsrest  24398  isfcf  24408  cnextfvval  24439  tmdgsum  24469  eltsms  24507  tsmsi  24508  tsmsgsum  24513  tsmssubm  24517  tsmsres  24518  tsmsf1o  24519  isust  24578  isucn  24651  isucn2  24652  ucnima  24654  imasdsf1olem  24747  metss  24882  met1stc  24895  metcnp  24915  metcnpi  24918  metcnpi2  24919  metucn  24945  xrge0tsms  25209  fsumcn  25246  elcncf  25265  cncfi  25270  rescncf  25273  cncfco  25283  caucfil  25659  equivcau  25676  caubl  25684  caublcls  25685  ovolgelb  25856  ovolunlem1a  25872  ovolicc2lem3  25895  voliunlem1  25926  voliunlem3  25928  volsuplem  25931  volsup  25932  dyadmax  25974  vitali  25989  itg2leub  26110  itgfsum  26202  dvnadd  26304  dvnres  26306  cpnord  26310  dvnfre  26327  dvmptfsum  26350  dvferm1  26360  dvferm2  26362  rolle  26365  dvlip  26368  c1lip1  26372  lhop1  26389  deg1leb  26468  ply1divex  26510  fta1g  26543  plyco  26615  dgrcolem1  26647  dgrco  26649  dvnply2  26663  plydivex  26673  rngunsnply  26693  aalioulem2  26717  aalioulem3  26718  aalioulem5  26720  aaliou3lem2  26727  dvntaylp  26755  taylthlem1  26757  ulmdvlem3  26786  abelthlem9  26824  cxpmul2  27074  scvxcvx  27370  jensenlem2  27372  jensen  27373  wilthlem3  27454  perfectlem2  27614  bcmono  27661  bposlem5  27672  lgsquad2lem2  27769  addsq2reu  27824  2sqreulem1  27830  2sqreunnlem1  27833  dchrisumlem1  27873  dchrisum0flb  27894  pntpbnd1  27970  pntlemf  27989  qabvle  28009  qabvexp  28010  ostthlem2  28012  ostth2lem2  28018  fltoprm  28052  nosupcbv  28116  nosupno  28117  nosupdm  28118  nosupfv  28120  nosupres  28121  nosupbnd1lem1  28122  nosupbnd1lem3  28124  nosupbnd1lem5  28126  noinfcbv  28131  noinfno  28132  noinfdm  28133  noinffv  28135  noinfres  28136  noinfbnd1lem3  28139  noinfbnd1lem5  28141  eqcuts2  28229  addsproplem1  28412  addsprop  28419  negsunif  28498  mulsproplem9  28567  sltmuls2  28591  precsexlem8  28657  precsexlem9  28658  precsexlem11  28660  noseqind  28735  om2noseqrdg  28747  noseqrdgfn  28749  n0addscl  28787  n0mulscl  28788  eucliddivs  28819  peano5uzs  28847  expscllem  28873  expadds  28878  expsne0  28879  expsgt0  28880  pw2cut  28903  pw2cut2  28905  bdaypw2n0bnd  28907  tgcgr4  29051  prlngmo2  29491  usgr2pth  30407  wlkiswwlks2lem4  30518  wlkiswwlks2  30521  rusgrnumwwlk  30624  clwlkclwwlklem2a  30646  clwlkclwwlklem1  30647  clwlkclwwlkfo  30657  eupth2  30897  frgr3vlem1  30931  3vfriswmgrlem  30935  3vfriswmgr  30936  wlkl0  31025  numclwlk2lem2f1o  31037  isplig  31135  isnvlem  31269  nvi  31273  nmoubi  31431  nmounbi  31435  nmblolbi  31459  ipasslem1  31490  ipassi  31500  hlim2  31851  pjhth  32052  spansni  32216  elspansn2  32226  pjige0  32350  pjcjt2  32351  pjopyth  32379  elcnop  32516  elcnfn  32541  nmopub  32567  cnopc  32572  nmfnleub  32584  elnlfn  32587  cnfnc  32589  nmbdoplb  32684  nmcexi  32685  nmcoplb  32689  lnfnmul  32707  nmbdfnlb  32709  nmcfnlb  32713  pjss2coi  32823  pjssmi  32824  isst  32872  ishst  32873  stcltr1i  32933  mdbr  32953  dmdbr  32958  mddmd2  32968  mdslmd1lem3  32986  mdslmd1lem4  32987  elat2  32999  atcvat2  33048  cdj1i  33092  iuninc  33253  fmptcof2  33349  nn0min  33508  nexple  33520  wrdt2ind  33612  ismnt  33643  xrge0tsmsd  33733  gsumwun  33736  cyc3genpm  33812  isarchi2  33845  archirng  33848  archiexdiv  33850  archiabl  33858  domnprodn0  33938  islbs5  34039  unitprodclb  34048  mxidlval  34090  1arithidom  34173  1arithufdlem3  34182  crefeq  34588  esumfzf  34812  issiga  34855  isrnsiga  34856  isldsys  34900  ismeas  34943  isrnmeas  34944  measiun  34962  eulerpartlemn  35124  sseqp1  35138  rrvsum  35197  signsply0  35291  signstfvc  35314  bnj941  35514  bnj106  35609  bnj155  35620  bnj590  35651  bnj591  35652  bnj849  35666  bnj893  35669  bnj944  35679  bnj1128  35731  eqhf  35861  tz9.1regs  35943  eqhfregs  35946  elkarden  35964  gblacfnacd  36070  subfacp1lem6  36158  erdszelem8  36171  issconn  36199  cvmliftlem7  36264  cvmliftlem10  36267  cvmlift3lem2  36293  satfsschain  36337  satfrel  36340  satfdm  36342  satfrnmapom  36343  fmlafvel  36358  satffun  36382  mrsubvrs  36495  mclsssvlem  36535  mclsval  36536  mclsax  36542  mclsind  36543  elpssmo  36673  shftvalg  36712  bccolsum  36719  iprodefisumlem  36720  faclimlem1  36723  rdgprc  36771  nmuladdss  37177  sbequbidv  37218  cbvsbdavw  37258  fveleq  37454  dfttc4lem1  37531  dfttc4  37533  elttcirr  37534  regsfromregtco  37541  mh-unprimbi  37547  unblimceq0  37588  bj-ax12  37771  bj-bm1.3ii  38249  rdgeqoa  38561  finxpreclem6  38587  domalom  38595  ralssiun  38598  wl-ax12v2cl  38697  wl-sblimt  38748  wl-sbhbt  38754  wl-2sb6d  38758  wl-mo2df  38770  wl-mo2t  38775  poimirlem2  38808  poimirlem25  38831  poimirlem28  38834  poimirlem31  38837  heicant  38841  mbfresfi  38852  itg2gt0cn  38861  sdclem2  38942  fdc  38945  seqpo  38947  incsequz  38948  mettrifi  38957  prdsbnd2  38995  heiborlem4  39014  bfplem1  39022  iscringd  39198  maxidlval  39239  igenval2  39266  iss2  39542  elrefrels3  39797  ax12eq  40264  ax12el  40265  ax12indalem  40268  ax12inda2ALT  40269  ax12inda  40271  ax12v2-o  40272  riotasvd  40279  isopos  40503  isat3  40630  ishlat1  40675  glbconN  40700  ispsubsp  41068  isldil  41433  isltrn  41442  isdilN  41477  trlval  41485  cdleme27b  41691  cdleme29b  41698  cdleme31sn1  41704  cdleme31sn1c  41711  cdleme40v  41792  cdlemk36  42236  cdlemkid5  42258  cdlemn11pre  42533  dihord2pre  42548  islpolN  42806  hdmapffval  43149  hdmapfval  43150  hdmapval2lem  43154  uzindd  43294  sticksstones1  43462  sticksstones2  43463  sticksstones3  43464  sticksstones8  43469  sticksstones10  43471  sticksstones11  43472  sticksstones12a  43473  sticksstones15  43477  indstrd  43509  unitscyglem3  43513  eu6w  43953  ismrc  43978  incssnn0  43988  mzpexpmpt  44022  pell14qrexpclnn0  44139  monotuz  44214  rmxypos  44220  jm2.17a  44233  jm2.17b  44234  rmygeid  44237  jm2.18  44261  jm2.19lem3  44264  jm2.25  44272  jm2.15nn0  44276  jm2.16nn0  44277  wepwsolem  44315  aomclem8  44329  dfac11  44330  pwslnm  44362  lnr2i  44383  hbtlem5  44395  unielss  44481  onsucf1lem  44532  cantnfresb  44587  onmcl  44594  naddonnn  44658  elmapintrab  44838  elmapintab  44857  cnvcnvintabd  44861  eliunov2  44940  relexpxpnnidm  44964  relexpiidm  44965  relexpss1d  44966  iunrelexpmin1  44969  relexpmulnn  44970  iunrelexpmin2  44973  relexp0a  44977  trclimalb2  44987  clsk3nimkb  45301  ntrclsiso  45328  ntrclskb  45330  ntrneiiso  45352  ntrneix2  45354  ntrneixb  45356  gneispace2  45393  gneispacess2  45407  mnuunid  45522  dvgrat  45557  pm14.122b  45667  relpeq1  46198  relpeq3  46200  trfr  46216  pwclaxpow  46238  prclaxpr  46239  uniclaxun  46240  modelac8prim  46246  permaxpow  46263  permaxpr  46264  permaxun  46265  nregmodel  46271  fnchoice  46320  fiiuncl  46356  ssinc  46375  ssdec  46376  wessf1ornlem  46473  dmrelrnrel  46512  fperiodmullem  46592  monoordxrv  46764  fmul01  46865  fmuldfeq  46868  climsuselem1  46892  climinff  46896  ellimcabssub0  46902  limcleqr  46927  addlimc  46931  0ellimcdiv  46932  limclner  46934  limsupref  46968  limsupub  46987  limsupmnf  47004  limsupre2lem  47007  limsupre2  47008  limsupre2mpt  47013  limsupre3lem  47015  limsupre3  47016  limsupre3mpt  47017  xlimbr  47110  cnrefiisplem  47112  dvnmptdivc  47221  dvnmptconst  47224  dvnmul  47226  iblspltprt  47256  itgspltprt  47262  stoweidlem2  47285  stoweidlem3  47286  stoweidlem17  47300  stoweidlem19  47302  stoweidlem21  47304  stoweidlem26  47309  fourierdlem42  47432  issal  47597  ismea  47734  isome  47777  carageniuncllem1  47804  caratheodorylem1  47809  2reu8i  48457  2reuimp0  48458  funressndmafv2rn  48566  2ffzoeq  48671  smonoord  48720  fargshiftf1  48796  ichnfimlem  48818  paireqne  48866  reupr  48877  reuopreuprim  48881  perfectALTVlem2  49093  grimcnv  49259  pgnbgreunbgrlem1  49484  pgnbgreunbgrlem4  49490  pgnbgreunbgr  49496  lmodvsmdi  49822  dmatALTval  49843  dmatALTbasel  49845  snlindsntor  49914  ldepsnlinc  49951  elbigo2r  49996  elbigolo1  50000  itcovalt2  50120  mof0  50280  isnrm4  50376  iscnrm3r  50393  iscnrm4  50399  lubsscl  50405  glbsscl  50406  ipolubdm  50432  ipoglbdm  50435  setrecseq  51194