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  915  19.23t  2211  axc14  2461  mojust  2532  mof  2556  eu6lem  2566  2gencl  3481  3gencl  3482  vtocl2gf  3529  vtocl3gf  3530  vtocl2g  3531  vtocl3g  3532  vtocl2ga  3535  vtocl2gaf  3536  vtocl3gaf  3538  vtocl3ga  3540  vtocl4g  3542  vtocl4ga  3543  eqeu  3668  mo2icl  3676  euind  3686  reu7  3694  reuind  3715  sbctt  3814  sbccomlem  3823  reu8nf  3831  sbcnestgfw  4374  sbcnestgf  4379  r19.36zv  4460  dedth2h  4538  dedth3h  4539  dedth4h  4540  reusngf  4628  reuprg0  4656  preq12bg  4807  elint  4905  elintrabg  4914  intab  4931  axrep1  5222  axreplem  5223  axrep2  5224  axrep6g  5232  bm1.3iiOLD  5244  reusv3  5347  swopolem  5541  solin  5558  freq1  5590  frminex  5602  vtoclr  5686  2optocl  5719  3optocl  5720  raliunxp  5786  resieq  5945  iss  5990  cnveqb  6149  reu3op  6244  reuop  6245  dfpo2  6248  preddowncl  6284  fnbrfvb  6877  fvelimab  6899  fvmptss  6946  fmptco  7067  fprg  7093  fnressn  7096  fressnfv  7098  isoselem  7282  ovg  7518  caovcan  7557  caovordig  7558  caovord  7564  tfisi  7799  tfindsg  7801  tfinds2  7804  tfinds3  7805  dfom2  7808  elom  7809  findsg  7837  finds2  7838  resf1extb  7874  f1o2ndf1  8062  poxp  8068  fnse  8073  xpord3inddlem  8094  soseq  8099  fpr3g  8225  frrlem12  8237  fpr2a  8242  wfr3g  8259  smoeq  8280  smores  8282  smogt  8297  tfrlem1  8305  tfr3  8328  oaordi  8471  oeordi  8512  oeoa  8522  oeoe  8524  nnacl  8536  nnmcl  8537  nnecl  8538  nnacom  8542  nnaordi  8543  nnawordi  8546  nnaass  8547  nndi  8548  nnmass  8549  nnmsucr  8550  nnmcom  8551  nnmordi  8556  naddssim  8610  naddoa  8627  2ecoptocl  8742  3ecoptocl  8743  undifixp  8868  xpdom2g  8997  findcard2  9088  unfi  9095  ssfi  9097  fnfi  9102  fodomfi  9219  imafiOLD  9223  xpfiOLD  9228  fodomfiOLD  9239  finsschain  9268  marypha1lem  9342  marypha1  9343  supeq1  9354  ordiso2  9426  ordtypelem7  9435  wemaplem1  9457  inf3lem2  9544  inf3lem5  9547  infdiffi  9573  cantnfval2  9584  cantnfle  9586  cantnfp1lem3  9595  oemapval  9598  cantnflem1  9604  cantnf  9608  wemapwe  9612  cnfcom  9615  cnfcom3clem  9620  ttrclss  9635  ttrclselem2  9641  tz9.1  9644  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  10507  axpowndlem3  10512  zfcndrep  10527  fpwwe2lem7  10550  pwfseqlem3  10573  wunr1om  10632  wunfi  10634  tskr1om  10680  ingru  10728  grudomon  10730  axgroth3  10744  axgroth4  10745  nqereu  10842  mulcanenq  10873  elnp  10900  elnpi  10901  prlem934  10946  infm3  12102  nnindd  12166  nnaddcl  12169  nnmulcl  12170  nnne0  12180  peano5uzi  12583  uzind2  12587  nn0indd  12591  zindd  12595  fzindd  12596  eluzaddOLD  12788  uzaddcl  12823  uzwo  12830  indstr  12835  zmax  12864  xmulasslem  13205  xrsupsslem  13227  xrinfmsslem  13228  xrsupss  13229  xrinfmss  13230  flval2  13736  om2uzlti  13875  uzrdgfni  13883  rabssnn0fi  13911  mptnn0fsupp  13922  seqcl2  13945  seqfveq2  13949  seqshft2  13953  monoord  13957  seqsplit  13960  seqcaopr3  13962  seqf1olem2a  13965  seqf1o  13968  seqid2  13973  seqhomo  13974  ser1const  13983  expcllem  13997  expeq0  14017  mulexp  14026  expadd  14029  expmul  14032  expmordi  14092  leexp2r  14099  leexp1a  14100  bernneq  14154  modexp  14163  facdiv  14212  faclbnd  14215  faclbnd4lem4  14221  hashgadd  14302  hashxp  14359  hashmap  14360  hashf1lem2  14381  hashf1  14382  seqcoll  14389  wrdind  14646  wrd2ind  14647  pfxccatin12lem3  14656  cshweqrep  14745  2cshwcshw  14750  relexp0g  14947  relexpsucnnr  14950  relexpsucnnl  14955  relexpcnv  14960  relexpnndm  14966  relexpaddnn  14976  rtrclreclem1  14982  dfrtrclrec2  14983  rtrclreclem2  14984  rtrclreclem4  14986  dfrtrcl2  14987  relexpind  14989  reusq0  15390  rlim  15420  rlim2  15421  rlim0  15433  rlim0lt  15434  rlimi  15438  ello12r  15442  ello1mpt  15446  ello1d  15448  elo12r  15453  lo1o1  15457  o1lo1  15462  lo1res  15484  climshft  15501  o1compt  15512  rlimo1  15542  lo1add  15552  lo1mul  15553  rlimdiv  15571  climub  15587  climserle  15588  caucvgrlem  15598  caurcvgr  15599  iseraltlem2  15608  summolem2a  15640  sumss  15649  fsum2d  15696  fsumabs  15726  fsumrlim  15736  fsumo1  15737  fsumiun  15746  binom  15755  climcndslem1  15774  climcndslem2  15775  cvgrat  15808  clim2prod  15813  prodfn0  15819  prodfrec  15820  ntrivcvgfvn0  15824  prodmolem2a  15859  fprodabs  15899  fprodn0  15904  fprod2d  15906  binomfallfac  15966  bpolycl  15977  bpolydif  15980  fprodefsum  16020  demoivreALT  16128  ruclem8  16164  ruclem9  16165  dvdsle  16239  dvdsfac  16255  divalglem7  16328  bitsinv1  16371  sadcadd  16387  sadadd2  16389  saddisjlem  16393  smuval2  16411  smupvallem  16412  smu01lem  16414  smupval  16417  smueqlem  16419  smumullem  16421  bezoutlem4  16471  dfgcd2  16475  rplpwr  16487  nn0seqcvgd  16499  seq1st  16500  alginv  16504  algcvga  16508  algfx  16509  lcmf  16562  prmind2  16614  prmdvdsexp  16644  prmfac1  16649  reumodprminv  16734  pcmpt  16822  pcfac  16829  prmpwdvds  16834  prmreclem4  16849  vdwlem10  16920  ramval  16938  ramcl  16959  cshwrepswhash1  17032  prmlem1a  17036  imasleval  17463  ismre  17510  mreexexd  17572  lubprop  18280  lublecllem  18282  glbprop  18293  joinlem  18305  meetlem  18319  poslubmo  18333  posglbmo  18334  poslubd  18335  isglbd  18433  lubun  18439  mndind  18720  frmdgsum  18754  mulgnnass  19006  mhmmulg  19012  gsumwrev  19263  gsmsymgrfix  19325  gsmsymgreq  19329  psgnunilem3  19393  sylow1lem1  19495  efginvrel2  19624  efgsrel  19631  efgredlemd  19641  efgredlem  19644  efgred  19645  efgrelexlemb  19647  gsum2dlem2  19868  gsumcom2  19872  ablfac1eulem  19971  pgpfac1lem2  19974  pgpfac1lem5  19978  pgpfac1  19979  pgpfac  19983  isomnd  20020  omndadd  20025  srgmulgass  20120  srgpcomp  20121  srgbinom  20134  isdomn2OLD  20615  isdomn3  20618  isorng  20764  lmodvsmmulgdi  20818  cnfldexp  21329  ofldchr  21501  islindf4  21763  assamulgscm  21826  mplcoe1  21960  mplcoe3  21961  mplcoe5  21963  gsummoncoe1  22211  dmatval  22395  dmatel  22396  dmatmulcl  22403  pmatcoe1fsupp  22604  decpmataa0  22671  decpmatmulsumfsupp  22676  pmatcollpw2lem  22680  pm2mpmhmlem1  22721  fiinopn  22804  mretopd  22995  neiptoptop  23034  cnpfval  23137  iscnp3  23147  tgcn  23155  lmbr  23161  lmbr2  23162  lmbrf  23163  lmss  23201  ishaus  23225  hausnei2  23256  t1sep2  23272  fiuncmp  23307  dfconn2  23322  1stcfb  23348  2ndc1stc  23354  1stcrest  23356  1stcelcls  23364  1stccn  23366  lly1stc  23399  elkgen  23439  kgencn  23459  tx1stc  23553  xkopt  23558  cnmptcom  23581  isr0  23640  r0sep  23651  ptcmpfi  23716  isfildlem  23760  rnelfm  23856  fbflim  23879  flimrest  23886  isflf  23896  flffbas  23898  lmflf  23908  fclsrest  23927  isfcf  23937  cnextfvval  23968  tmdgsum  23998  eltsms  24036  tsmsi  24037  tsmsgsum  24042  tsmssubm  24046  tsmsres  24047  tsmsf1o  24048  isust  24107  isucn  24181  isucn2  24182  ucnima  24184  imasdsf1olem  24277  metss  24412  met1stc  24425  metcnp  24445  metcnpi  24448  metcnpi2  24449  metucn  24475  xrge0tsms  24739  fsumcn  24777  elcncf  24798  cncfi  24803  rescncf  24806  cncfco  24816  caucfil  25199  equivcau  25216  caubl  25224  caublcls  25225  ovolgelb  25397  ovolunlem1a  25413  ovolicc2lem3  25436  voliunlem1  25467  voliunlem3  25469  volsuplem  25472  volsup  25473  dyadmax  25515  vitali  25530  itg2leub  25651  itgfsum  25744  dvnadd  25847  dvnres  25849  cpnord  25853  dvnfre  25872  dvmptfsum  25895  dvferm1  25905  dvferm2  25907  rolle  25910  dvlip  25914  c1lip1  25918  lhop1  25935  deg1leb  26016  ply1divex  26058  fta1g  26091  plyco  26162  dgrcolem1  26195  dgrco  26197  dvnply2  26211  plydivex  26221  aalioulem2  26257  aalioulem3  26258  aalioulem5  26260  aaliou3lem2  26267  dvntaylp  26295  taylthlem1  26297  ulmdvlem3  26327  abelthlem9  26366  cxpmul2  26614  scvxcvx  26912  jensenlem2  26914  jensen  26915  wilthlem3  26996  perfectlem2  27157  bcmono  27204  bposlem5  27215  lgsquad2lem2  27312  addsq2reu  27367  2sqreulem1  27373  2sqreunnlem1  27376  dchrisumlem1  27416  dchrisum0flb  27437  pntpbnd1  27513  pntlemf  27532  qabvle  27552  qabvexp  27553  ostthlem2  27555  ostth2lem2  27561  nosupcbv  27630  nosupno  27631  nosupdm  27632  nosupfv  27634  nosupres  27635  nosupbnd1lem1  27636  nosupbnd1lem3  27638  nosupbnd1lem5  27640  noinfcbv  27645  noinfno  27646  noinfdm  27647  noinffv  27649  noinfres  27650  noinfbnd1lem3  27653  noinfbnd1lem5  27655  eqscut2  27735  addsproplem1  27899  addsprop  27906  negsunif  27984  mulsproplem9  28050  ssltmul2  28074  precsexlem8  28139  precsexlem9  28140  precsexlem11  28142  noseqind  28209  om2noseqrdg  28221  noseqrdgfn  28223  n0addscl  28259  n0mulscl  28260  eucliddivs  28288  peano5uzs  28315  expscllem  28340  expadds  28345  expsne0  28346  expsgt0  28347  pw2cut  28366  tgcgr4  28494  usgr2pth  29727  wlkiswwlks2lem4  29835  wlkiswwlks2  29838  rusgrnumwwlk  29938  clwlkclwwlklem2a  29960  clwlkclwwlklem1  29961  clwlkclwwlkfo  29971  eupth2  30201  frgr3vlem1  30235  3vfriswmgrlem  30239  3vfriswmgr  30240  wlkl0  30329  numclwlk2lem2f1o  30341  isplig  30438  isnvlem  30572  nvi  30576  nmoubi  30734  nmounbi  30738  nmblolbi  30762  ipasslem1  30793  ipassi  30803  hlim2  31154  pjhth  31355  spansni  31519  elspansn2  31529  pjige0  31653  pjcjt2  31654  pjopyth  31682  elcnop  31819  elcnfn  31844  nmopub  31870  cnopc  31875  nmfnleub  31887  elnlfn  31890  cnfnc  31892  nmbdoplb  31987  nmcexi  31988  nmcoplb  31992  lnfnmul  32010  nmbdfnlb  32012  nmcfnlb  32016  pjss2coi  32126  pjssmi  32127  isst  32175  ishst  32176  stcltr1i  32236  mdbr  32256  dmdbr  32261  mddmd2  32271  mdslmd1lem3  32289  mdslmd1lem4  32290  elat2  32302  atcvat2  32351  cdj1i  32395  iuninc  32522  fmptcof2  32614  nn0min  32778  nexple  32802  wrdt2ind  32908  ismnt  32938  xrge0tsmsd  33028  gsumwun  33031  cyc3genpm  33107  isarchi2  33140  archirng  33143  archiexdiv  33145  archiabl  33153  domnprodn0  33228  islbs5  33330  unitprodclb  33339  mxidlval  33411  1arithidom  33487  1arithufdlem3  33496  crefeq  33814  esumfzf  34038  issiga  34081  isrnsiga  34082  isldsys  34125  ismeas  34168  isrnmeas  34169  measiun  34187  eulerpartlemn  34351  sseqp1  34365  rrvsum  34424  signsply0  34521  signstfvc  34544  bnj941  34741  bnj106  34837  bnj155  34848  bnj590  34879  bnj591  34880  bnj849  34894  bnj893  34897  bnj944  34907  bnj1128  34959  tz9.1regs  35069  gblacfnacd  35077  subfacp1lem6  35160  erdszelem8  35173  issconn  35201  cvmliftlem7  35266  cvmliftlem10  35269  cvmlift3lem2  35295  satfsschain  35339  satfrel  35342  satfdm  35344  satfrnmapom  35345  fmlafvel  35360  satffun  35384  mrsubvrs  35497  mclsssvlem  35537  mclsval  35538  mclsax  35544  mclsind  35545  shftvalg  35707  bccolsum  35714  iprodefisumlem  35715  faclimlem1  35718  rdgprc  35770  sbequbidv  36190  cbvsbdavw  36230  fveleq  36427  unblimceq0  36483  bj-ax12  36633  bj-bm1.3ii  37040  rdgeqoa  37346  finxpreclem6  37372  domalom  37380  ralssiun  37383  wl-ax12v2cl  37482  wl-sblimt  37524  wl-sbhbt  37530  wl-2sb6d  37534  wl-mo2df  37546  wl-mo2t  37551  poimirlem2  37604  poimirlem25  37627  poimirlem28  37630  poimirlem31  37633  heicant  37637  mbfresfi  37648  itg2gt0cn  37657  sdclem2  37724  fdc  37727  seqpo  37729  incsequz  37730  mettrifi  37739  prdsbnd2  37777  heiborlem4  37796  bfplem1  37804  iscringd  37980  maxidlval  38021  igenval2  38048  iss2  38314  elrefrels3  38498  ax12eq  38922  ax12el  38923  ax12indalem  38926  ax12inda2ALT  38927  ax12inda  38929  ax12v2-o  38930  riotasvd  38937  isopos  39161  isat3  39288  ishlat1  39333  glbconN  39358  glbconNOLD  39359  ispsubsp  39727  isldil  40092  isltrn  40101  isdilN  40136  trlval  40144  cdleme27b  40350  cdleme29b  40357  cdleme31sn1  40363  cdleme31sn1c  40370  cdleme40v  40451  cdlemk36  40895  cdlemkid5  40917  cdlemn11pre  41192  dihord2pre  41207  islpolN  41465  hdmapffval  41808  hdmapfval  41809  hdmapval2lem  41813  uzindd  41953  sticksstones1  42122  sticksstones2  42123  sticksstones3  42124  sticksstones8  42129  sticksstones10  42131  sticksstones11  42132  sticksstones12a  42133  sticksstones15  42137  indstrd  42169  unitscyglem3  42173  nnaddcom  42244  nnadddir  42246  nnmulcom  42248  eu6w  42652  ismrc  42677  incssnn0  42687  mzpexpmpt  42721  pell14qrexpclnn0  42842  monotuz  42917  rmxypos  42923  jm2.17a  42936  jm2.17b  42937  rmygeid  42940  jm2.18  42964  jm2.19lem3  42967  jm2.25  42975  jm2.15nn0  42979  jm2.16nn0  42980  wepwsolem  43018  aomclem8  43037  dfac11  43038  pwslnm  43070  lnr2i  43092  hbtlem5  43104  cnsrexpcl  43141  rngunsnply  43145  unielss  43194  onsucf1lem  43245  cantnfresb  43300  onmcl  43307  naddonnn  43371  elmapintrab  43552  elmapintab  43572  cnvcnvintabd  43576  eliunov2  43655  relexpxpnnidm  43679  relexpiidm  43680  relexpss1d  43681  iunrelexpmin1  43684  relexpmulnn  43685  iunrelexpmin2  43688  relexp0a  43692  trclimalb2  43702  clsk3nimkb  44016  ntrclsiso  44043  ntrclskb  44045  ntrneiiso  44067  ntrneix2  44069  ntrneixb  44071  gneispace2  44108  gneispacess2  44122  mnuunid  44253  dvgrat  44288  pm14.122b  44399  relpeq1  44921  relpeq3  44923  trfr  44939  pwclaxpow  44961  prclaxpr  44962  uniclaxun  44963  modelac8prim  44969  permaxpow  44986  permaxpr  44987  permaxun  44988  nregmodel  44994  fnchoice  45010  fiiuncl  45046  ssinc  45068  ssdec  45069  wessf1ornlem  45166  dmrelrnrel  45207  fperiodmullem  45288  monoordxrv  45464  fmul01  45565  fmuldfeq  45568  climsuselem1  45592  climinff  45596  ellimcabssub0  45602  limcleqr  45629  addlimc  45633  0ellimcdiv  45634  limclner  45636  limsupref  45670  limsupub  45689  limsupmnf  45706  limsupre2lem  45709  limsupre2  45710  limsupre2mpt  45715  limsupre3lem  45717  limsupre3  45718  limsupre3mpt  45719  xlimbr  45812  cnrefiisplem  45814  dvnmptdivc  45923  dvnmptconst  45926  dvnmul  45928  iblspltprt  45958  itgspltprt  45964  stoweidlem2  45987  stoweidlem3  45988  stoweidlem17  46002  stoweidlem19  46004  stoweidlem21  46006  stoweidlem26  46011  fourierdlem42  46134  issal  46299  ismea  46436  isome  46479  carageniuncllem1  46506  caratheodorylem1  46511  2reu8i  47101  2reuimp0  47102  funressndmafv2rn  47211  2ffzoeq  47315  smonoord  47359  fargshiftf1  47429  ichnfimlem  47451  paireqne  47499  reupr  47510  reuopreuprim  47514  perfectALTVlem2  47710  grimcnv  47876  pgnbgreunbgrlem1  48101  pgnbgreunbgrlem4  48107  pgnbgreunbgr  48113  lmodvsmdi  48367  dmatALTval  48389  dmatALTbasel  48391  snlindsntor  48460  ldepsnlinc  48497  elbigo2r  48542  elbigolo1  48546  itcovalt2  48666  mof0  48826  isnrm4  48919  iscnrm3r  48936  iscnrm4  48942  lubsscl  48948  glbsscl  48949  ipolubdm  48975  ipoglbdm  48978  setrecseq  49674  setrec2fun  49681  setrec2lem2  49683