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  2246  axc14  2492  mojust  2563  mof  2588  eu6lem  2598  2gencl  3492  3gencl  3493  vtocl2gf  3531  vtocl3gf  3532  vtocl2g  3533  vtocl3g  3534  vtocl2ga  3537  vtocl2gaf  3538  vtocl3gaf  3539  vtocl3ga  3540  vtocl4g  3541  vtocl4ga  3542  eqeu  3663  mo2icl  3671  euind  3681  reu7  3689  reuind  3710  sbctt  3807  sbccomlem  3817  reu8nf  3824  sbcnestgfw  4378  sbcnestgf  4383  r19.36zv  4467  dedth2h  4541  dedth3h  4542  dedth4h  4543  reusngf  4631  reuprg0  4659  preq12bg  4807  elint  4912  elintrabg  4920  intab  4937  axrep1  5232  axreplem  5233  axrep2  5234  axrep6g  5242  reusv3  5367  swopolem  5569  solin  5586  freq1  5618  frminex  5630  vtoclr  5714  2optocl  5748  3optocl  5749  raliunxp  5817  resieq  5982  iss  6029  reu3op  6298  reuop  6299  dfpo2  6302  preddowncl  6338  fnbrfvb  6940  fvelimab  6962  fvmptss  7011  fmptco  7135  fprg  7164  fnressn  7167  fressnfv  7169  isoselem  7353  ovg  7589  caovcan  7629  caovordig  7630  caovord  7636  tfisi  7874  tfindsg  7876  tfinds2  7879  tfinds3  7880  dfom2  7883  elom  7884  findsg  7913  finds2  7914  resf1extb  7950  f1o2ndf1  8139  poxp  8146  fnse  8156  xpord3inddlem  8177  soseq  8182  fpr3g  8310  frrlem12  8322  fpr2a  8327  wfr3g  8344  smoeq  8365  smores  8367  smogt  8382  tfrlem1  8390  tfr3  8414  tz7.48lem  8457  oaordi  8561  oeordi  8603  oeoa  8613  oeoe  8615  nnacl  8627  nnmcl  8628  nnecl  8629  nnacom  8633  nnaordi  8634  nnawordi  8637  nnaass  8638  nndi  8639  nnmass  8640  nnmsucr  8641  nnmcom  8642  nnmordi  8647  naddssim  8702  naddoa  8719  2ecoptocl  8836  3ecoptocl  8837  undifixp  8969  xpdom2g  9099  findcard2  9187  unfi  9193  ssfi  9195  fnfi  9200  fodomfi  9311  finsschain  9355  marypha1lem  9432  marypha1  9433  supeq1  9444  ordiso2  9516  ordtypelem7  9525  wemaplem1  9547  inf3lem2  9637  inf3lem5  9640  infdiffi  9666  cantnfval2  9677  cantnfle  9679  cantnfp1lem3  9688  oemapval  9691  cantnflem1  9697  cantnf  9701  wemapwe  9705  cnfcom  9708  cnfcom3clem  9713  ttrclss  9728  ttrclselem2  9734  tz9.1  9737  frr3g  9767  frr2  9771  r1pwALT  9867  r1filimi  9910  cplem2  9959  cplem2OLD  9960  kardenOLD  9967  setrec2fun  9980  setrec2lem2  9983  updjud  10022  infxpenc2lem2  10106  fseqenlem1  10110  dfac8clem  10118  alephinit  10181  dfac4  10208  dfac5lem5  10213  dfac2a  10215  dfac2b  10216  dfacacn  10227  dfac12lem3  10231  kmlem2  10237  kmlem13  10248  nnadju  10283  ackbij1lem16  10319  sornom  10362  infpssrlem4  10391  fin23lem14  10418  fin23lem32  10429  fin23lem34  10431  fin23lem36  10433  isf32lem1  10438  isf32lem2  10439  axcc2lem  10521  axcc3  10523  axcclem  10542  zornn0g  10590  ttukeylem5  10598  ttukeylem6  10599  axrepnd  10686  axpowndlem3  10691  zfcndrep  10706  fpwwe2lem7  10729  pwfseqlem3  10752  wunr1om  10811  wunfi  10813  tskr1om  10859  ingru  10907  grudomon  10909  axgroth3  10923  axgroth4  10924  nqereu  11021  mulcanenq  11052  elnp  11079  elnpi  11080  prlem934  11125  infm3  12283  nnindd  12362  nnaddcl  12365  nnmulcl  12366  nnaddcom  12369  nnne0  12379  nnadddir  12401  nnmulcom  12403  peano5uzi  12795  uzind2  12799  nn0indd  12803  zindd  12807  fzindd  12808  uzaddcl  13038  uzwo  13045  indstr  13050  zmax  13079  xmulasslem  13422  xrsupsslem  13444  xrinfmsslem  13445  xrsupss  13446  xrinfmss  13447  flval2  13961  om2uzlti  14100  uzrdgfni  14108  rabssnn0fi  14136  mptnn0fsupp  14147  seqcl2  14170  seqfveq2  14174  seqshft2  14178  monoord  14182  seqsplit  14185  seqcaopr3  14187  seqf1olem2a  14190  seqf1o  14193  seqid2  14198  seqhomo  14199  ser1const  14208  expcllem  14222  expeq0  14242  mulexp  14251  expadd  14254  expmul  14257  expmordi  14317  leexp2r  14324  leexp1a  14325  bernneq  14380  modexp  14389  facdiv  14438  faclbnd  14441  faclbnd4lem4  14447  hashgadd  14528  hashxp  14586  hashmap  14587  hashf1lem2  14608  hashf1  14609  seqcoll  14616  wrdind  14879  wrd2ind  14880  pfxccatin12lem3  14889  cshweqrep  14980  2cshwcshw  14984  relexp0g  15184  relexpsucnnr  15187  relexpsucnnl  15192  relexpcnv  15197  relexpnndm  15203  relexpaddnn  15213  rtrclreclem1  15219  dfrtrclrec2  15220  rtrclreclem2  15221  rtrclreclem4  15223  dfrtrcl2  15224  relexpind  15226  reusq0  15641  rlim  15671  rlim2  15672  rlim0  15684  rlim0lt  15685  rlimi  15689  ello12r  15693  ello1mpt  15697  ello1d  15699  elo12r  15704  lo1o1  15708  o1lo1  15713  lo1res  15735  climshft  15752  o1compt  15763  rlimo1  15793  lo1add  15803  lo1mul  15804  rlimdiv  15822  climub  15838  climserle  15839  caucvgrlem  15849  caurcvgr  15850  iseraltlem2  15859  summolem2a  15890  sumss  15899  fsum2d  15946  fsumabs  15977  fsumrlim  15987  fsumo1  15988  fsumiun  15997  binom  16008  climcndslem1  16027  climcndslem2  16028  cvgrat  16061  clim2prod  16066  prodfn0  16072  prodfrec  16073  ntrivcvgfvn0  16077  prodmolem2a  16110  fprodabs  16150  fprodn0  16155  fprod2d  16157  binomfallfac  16216  bpolycl  16227  bpolydif  16230  fprodefsum  16270  demoivreALT  16378  ruclem8  16414  ruclem9  16415  dvdsle  16489  dvdsfac  16505  divalglem7  16578  bitsinv1  16621  sadcadd  16637  sadadd2  16639  saddisjlem  16643  smuval2  16661  smupvallem  16662  smu01lem  16664  smupval  16667  smueqlem  16669  smumullem  16671  bezoutlem4  16724  dfgcd2  16728  rplpwr  16741  nn0seqcvgd  16754  seq1st  16755  alginv  16759  algcvga  16763  algfx  16764  lcmf  16817  prmind2  16869  prmdvdsexp  16900  prmfac1  16905  reumodprminv  16991  pcmpt  17079  pcfac  17086  prmpwdvds  17091  prmreclem4  17106  vdwlem10  17177  ramval  17195  ramcl  17216  cshwrepswhash1  17289  prmlem1a  17293  imasleval  17722  ismre  17769  mreexexd  17831  lubprop  18539  lublecllem  18541  glbprop  18552  joinlem  18564  meetlem  18578  poslubmo  18592  posglbmo  18593  poslubd  18594  isglbd  18692  lubun  18698  mndind  19033  frmdgsum  19067  mulgnnass  19328  mhmmulg  19334  gsumwrev  19589  gsmsymgrfix  19651  gsmsymgreq  19655  psgnunilem3  19719  sylow1lem1  19821  efginvrel2  19950  efgsrel  19957  efgredlemd  19967  efgredlem  19970  efgred  19971  efgrelexlemb  19973  gsum2dlem2  20194  gsumcom2  20198  ablfac1eulem  20297  pgpfac1lem2  20300  pgpfac1lem5  20304  pgpfac1  20305  pgpfac  20309  isomnd  20346  omndadd  20351  srgmulgass  20452  srgpcomp  20453  srgbinom  20466  isdomn3  20975  isorng  21127  lmodvsmmulgdi  21181  rspprop  21533  cnfldexp  21720  ofldchr  21891  islindf4  22153  assamulgscm  22218  mplcoe1  22355  mplcoe3  22356  mplcoe5  22358  gsummoncoe1  22635  dmatval  22816  dmatel  22817  dmatmulcl  22824  pmatcoe1fsupp  23028  decpmataa0  23095  decpmatmulsumfsupp  23100  pmatcollpw2lem  23104  pm2mpmhmlem1  23145  fiinopn  23228  mretopd  23419  neiptoptop  23458  cnpfval  23561  iscnp3  23571  tgcn  23579  lmbr  23585  lmbr2  23586  lmbrf  23587  lmss  23625  ishaus  23649  hausnei2  23680  t1sep2  23696  fiuncmp  23731  dfconn2  23746  1stcfb  23772  2ndc1stc  23778  1stcrest  23780  1stcelcls  23789  1stccn  23791  lly1stc  23824  elkgen  23864  kgencn  23884  tx1stc  23978  xkopt  23983  cnmptcom  24006  isr0  24065  r0sep  24076  ptcmpfi  24141  isfildlem  24185  rnelfm  24281  fbflim  24304  flimrest  24311  isflf  24321  flffbas  24323  lmflf  24333  fclsrest  24352  isfcf  24362  cnextfvval  24393  tmdgsum  24423  eltsms  24461  tsmsi  24462  tsmsgsum  24467  tsmssubm  24471  tsmsres  24472  tsmsf1o  24473  isust  24532  isucn  24605  isucn2  24606  ucnima  24608  imasdsf1olem  24701  metss  24836  met1stc  24849  metcnp  24869  metcnpi  24872  metcnpi2  24873  metucn  24899  xrge0tsms  25163  fsumcn  25200  elcncf  25219  cncfi  25224  rescncf  25227  cncfco  25237  caucfil  25613  equivcau  25630  caubl  25638  caublcls  25639  ovolgelb  25810  ovolunlem1a  25826  ovolicc2lem3  25849  voliunlem1  25880  voliunlem3  25882  volsuplem  25885  volsup  25886  dyadmax  25928  vitali  25943  itg2leub  26064  itgfsum  26156  dvnadd  26258  dvnres  26260  cpnord  26264  dvnfre  26281  dvmptfsum  26304  dvferm1  26314  dvferm2  26316  rolle  26319  dvlip  26322  c1lip1  26326  lhop1  26343  deg1leb  26422  ply1divex  26464  fta1g  26497  plyco  26569  dgrcolem1  26601  dgrco  26603  dvnply2  26617  plydivex  26627  aalioulem2  26669  aalioulem3  26670  aalioulem5  26672  aaliou3lem2  26679  dvntaylp  26707  taylthlem1  26709  ulmdvlem3  26738  abelthlem9  26776  cxpmul2  27026  scvxcvx  27322  jensenlem2  27324  jensen  27325  wilthlem3  27406  perfectlem2  27566  bcmono  27613  bposlem5  27624  lgsquad2lem2  27721  addsq2reu  27776  2sqreulem1  27782  2sqreunnlem1  27785  dchrisumlem1  27825  dchrisum0flb  27846  pntpbnd1  27922  pntlemf  27941  qabvle  27961  qabvexp  27962  ostthlem2  27964  ostth2lem2  27970  fltoprm  28004  nosupcbv  28068  nosupno  28069  nosupdm  28070  nosupfv  28072  nosupres  28073  nosupbnd1lem1  28074  nosupbnd1lem3  28076  nosupbnd1lem5  28078  noinfcbv  28083  noinfno  28084  noinfdm  28085  noinffv  28087  noinfres  28088  noinfbnd1lem3  28091  noinfbnd1lem5  28093  eqcuts2  28181  addsproplem1  28364  addsprop  28371  negsunif  28450  mulsproplem9  28519  sltmuls2  28543  precsexlem8  28609  precsexlem9  28610  precsexlem11  28612  noseqind  28687  om2noseqrdg  28699  noseqrdgfn  28701  n0addscl  28739  n0mulscl  28740  eucliddivs  28771  peano5uzs  28799  expscllem  28825  expadds  28830  expsne0  28831  expsgt0  28832  pw2cut  28855  pw2cut2  28857  bdaypw2n0bnd  28859  tgcgr4  29003  prlngmo2  29443  usgr2pth  30359  wlkiswwlks2lem4  30470  wlkiswwlks2  30473  rusgrnumwwlk  30576  clwlkclwwlklem2a  30598  clwlkclwwlklem1  30599  clwlkclwwlkfo  30609  eupth2  30849  frgr3vlem1  30883  3vfriswmgrlem  30887  3vfriswmgr  30888  wlkl0  30977  numclwlk2lem2f1o  30989  isplig  31087  isnvlem  31221  nvi  31225  nmoubi  31383  nmounbi  31387  nmblolbi  31411  ipasslem1  31442  ipassi  31452  hlim2  31803  pjhth  32004  spansni  32168  elspansn2  32178  pjige0  32302  pjcjt2  32303  pjopyth  32331  elcnop  32468  elcnfn  32493  nmopub  32519  cnopc  32524  nmfnleub  32536  elnlfn  32539  cnfnc  32541  nmbdoplb  32636  nmcexi  32637  nmcoplb  32641  lnfnmul  32659  nmbdfnlb  32661  nmcfnlb  32665  pjss2coi  32775  pjssmi  32776  isst  32824  ishst  32825  stcltr1i  32885  mdbr  32905  dmdbr  32910  mddmd2  32920  mdslmd1lem3  32938  mdslmd1lem4  32939  elat2  32951  atcvat2  33000  cdj1i  33044  iuninc  33206  fmptcof2  33302  nn0min  33462  nexple  33474  wrdt2ind  33566  ismnt  33594  xrge0tsmsd  33684  gsumwun  33687  cyc3genpm  33763  isarchi2  33796  archirng  33799  archiexdiv  33801  archiabl  33809  domnprodn0  33889  islbs5  33985  unitprodclb  33994  mxidlval  34036  1arithidom  34119  1arithufdlem3  34128  crefeq  34527  esumfzf  34751  issiga  34794  isrnsiga  34795  isldsys  34839  ismeas  34882  isrnmeas  34883  measiun  34901  eulerpartlemn  35063  sseqp1  35077  rrvsum  35136  signsply0  35230  signstfvc  35253  bnj941  35453  bnj106  35548  bnj155  35559  bnj590  35590  bnj591  35591  bnj849  35605  bnj893  35608  bnj944  35618  bnj1128  35670  r1omhfb  35794  tz9.1regs  35862  r1omhfbregs  35865  elkarden  35883  gblacfnacd  35952  subfacp1lem6  36040  erdszelem8  36053  issconn  36081  cvmliftlem7  36146  cvmliftlem10  36149  cvmlift3lem2  36175  satfsschain  36219  satfrel  36222  satfdm  36224  satfrnmapom  36225  fmlafvel  36240  satffun  36264  mrsubvrs  36377  mclsssvlem  36417  mclsval  36418  mclsax  36424  mclsind  36425  shftvalg  36593  bccolsum  36600  iprodefisumlem  36601  faclimlem1  36604  rdgprc  36652  nmuladdss  37058  sbequbidv  37099  cbvsbdavw  37139  fveleq  37335  dfttc4lem1  37412  dfttc4  37414  elttcirr  37415  regsfromregtco  37422  mh-unprimbi  37428  unblimceq0  37469  bj-ax12  37652  bj-bm1.3ii  38087  rdgeqoa  38402  finxpreclem6  38428  domalom  38436  ralssiun  38439  wl-ax12v2cl  38538  wl-sblimt  38589  wl-sbhbt  38595  wl-2sb6d  38599  wl-mo2df  38611  wl-mo2t  38616  poimirlem2  38649  poimirlem25  38672  poimirlem28  38675  poimirlem31  38678  heicant  38682  mbfresfi  38693  itg2gt0cn  38702  sdclem2  38785  fdc  38788  seqpo  38790  incsequz  38791  mettrifi  38800  prdsbnd2  38838  heiborlem4  38857  bfplem1  38865  iscringd  39041  maxidlval  39082  igenval2  39109  iss2  39385  elrefrels3  39640  ax12eq  40107  ax12el  40108  ax12indalem  40111  ax12inda2ALT  40112  ax12inda  40114  ax12v2-o  40115  riotasvd  40122  isopos  40346  isat3  40473  ishlat1  40518  glbconN  40543  ispsubsp  40911  isldil  41276  isltrn  41285  isdilN  41320  trlval  41328  cdleme27b  41534  cdleme29b  41541  cdleme31sn1  41547  cdleme31sn1c  41554  cdleme40v  41635  cdlemk36  42079  cdlemkid5  42101  cdlemn11pre  42376  dihord2pre  42391  islpolN  42649  hdmapffval  42992  hdmapfval  42993  hdmapval2lem  42997  uzindd  43137  sticksstones1  43305  sticksstones2  43306  sticksstones3  43307  sticksstones8  43312  sticksstones10  43314  sticksstones11  43315  sticksstones12a  43316  sticksstones15  43320  indstrd  43352  unitscyglem3  43356  eu6w  43796  ismrc  43821  incssnn0  43831  mzpexpmpt  43865  pell14qrexpclnn0  43982  monotuz  44057  rmxypos  44063  jm2.17a  44076  jm2.17b  44077  rmygeid  44080  jm2.18  44104  jm2.19lem3  44107  jm2.25  44115  jm2.15nn0  44119  jm2.16nn0  44120  wepwsolem  44158  aomclem8  44172  dfac11  44173  pwslnm  44205  lnr2i  44227  hbtlem5  44239  cnsrexpcl  44276  rngunsnply  44280  unielss  44329  onsucf1lem  44380  cantnfresb  44435  onmcl  44442  naddonnn  44506  elmapintrab  44686  elmapintab  44705  cnvcnvintabd  44709  eliunov2  44788  relexpxpnnidm  44812  relexpiidm  44813  relexpss1d  44814  iunrelexpmin1  44817  relexpmulnn  44818  iunrelexpmin2  44821  relexp0a  44825  trclimalb2  44835  clsk3nimkb  45149  ntrclsiso  45176  ntrclskb  45178  ntrneiiso  45200  ntrneix2  45202  ntrneixb  45204  gneispace2  45241  gneispacess2  45255  mnuunid  45370  dvgrat  45405  pm14.122b  45515  relpeq1  46042  relpeq3  46044  trfr  46060  pwclaxpow  46082  prclaxpr  46083  uniclaxun  46084  modelac8prim  46090  permaxpow  46107  permaxpr  46108  permaxun  46109  nregmodel  46115  fnchoice  46154  fiiuncl  46190  ssinc  46210  ssdec  46211  wessf1ornlem  46308  dmrelrnrel  46347  fperiodmullem  46427  monoordxrv  46599  fmul01  46700  fmuldfeq  46703  climsuselem1  46727  climinff  46731  ellimcabssub0  46737  limcleqr  46762  addlimc  46766  0ellimcdiv  46767  limclner  46769  limsupref  46803  limsupub  46822  limsupmnf  46839  limsupre2lem  46842  limsupre2  46843  limsupre2mpt  46848  limsupre3lem  46850  limsupre3  46851  limsupre3mpt  46852  xlimbr  46945  cnrefiisplem  46947  dvnmptdivc  47056  dvnmptconst  47059  dvnmul  47061  iblspltprt  47091  itgspltprt  47097  stoweidlem2  47120  stoweidlem3  47121  stoweidlem17  47135  stoweidlem19  47137  stoweidlem21  47139  stoweidlem26  47144  fourierdlem42  47267  issal  47432  ismea  47569  isome  47612  carageniuncllem1  47639  caratheodorylem1  47644  2reu8i  48292  2reuimp0  48293  funressndmafv2rn  48401  2ffzoeq  48506  smonoord  48555  fargshiftf1  48631  ichnfimlem  48653  paireqne  48701  reupr  48712  reuopreuprim  48716  perfectALTVlem2  48928  grimcnv  49094  pgnbgreunbgrlem1  49319  pgnbgreunbgrlem4  49325  pgnbgreunbgr  49331  lmodvsmdi  49599  dmatALTval  49620  dmatALTbasel  49622  snlindsntor  49691  ldepsnlinc  49728  elbigo2r  49773  elbigolo1  49777  itcovalt2  49897  mof0  50057  isnrm4  50153  iscnrm3r  50170  iscnrm4  50176  lubsscl  50182  glbsscl  50183  ipolubdm  50209  ipoglbdm  50212  setrecseq  50971