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 ⊢ (𝜑 → ((𝜃 → 𝜓) ↔ (𝜃 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  imbi12d  347  imbi2  351  pm5.42  552  orbi2d  928  19.23t  2252  axc14  2501  mojust  2572  mof  2597  eu6lem  2607  2gencl  3505  3gencl  3506  vtocl2gf  3545  vtocl3gf  3546  vtocl2g  3547  vtocl3g  3548  vtocl2ga  3551  vtocl2gaf  3552  vtocl3gaf  3553  vtocl3ga  3554  vtocl4g  3555  vtocl4ga  3556  eqeu  3678  mo2icl  3686  euind  3696  reu7  3704  reuind  3725  sbctt  3822  sbccomlem  3831  reu8nf  3839  sbcnestgfw  4384  sbcnestgf  4389  r19.36zv  4475  dedth2h  4549  dedth3h  4550  dedth4h  4551  reusngf  4642  reuprg0  4670  preq12bg  4819  elint  4919  elintrabg  4927  intab  4944  axrep1  5240  axreplem  5241  axrep2  5242  axrep6g  5252  bm1.3iiOLD  5264  reusv3  5374  swopolem  5577  solin  5594  freq1  5626  frminex  5638  vtoclr  5722  2optocl  5755  3optocl  5756  raliunxp  5823  resieq  5987  iss  6035  cnveqb  6193  reu3op  6291  reuop  6292  dfpo2  6295  preddowncl  6331  fnbrfvb  6929  fvelimab  6951  fvmptss  7000  fmptco  7123  fprg  7150  fnressn  7153  fressnfv  7155  isoselem  7337  ovg  7573  caovcan  7612  caovordig  7613  caovord  7619  tfisi  7851  tfindsg  7853  tfinds2  7856  tfinds3  7857  dfom2  7860  elom  7861  findsg  7890  finds2  7891  resf1extb  7927  f1o2ndf1  8113  poxp  8120  fnse  8125  xpord3inddlem  8146  soseq  8151  fpr3g  8278  frrlem12  8290  fpr2a  8295  wfr3g  8312  smoeq  8333  smores  8335  smogt  8350  tfrlem1  8358  tfr3  8382  oaordi  8527  oeordi  8569  oeoa  8579  oeoe  8581  nnacl  8593  nnmcl  8594  nnecl  8595  nnacom  8599  nnaordi  8600  nnawordi  8603  nnaass  8604  nndi  8605  nnmass  8606  nnmsucr  8607  nnmcom  8608  nnmordi  8613  naddssim  8668  naddoa  8685  2ecoptocl  8802  3ecoptocl  8803  undifixp  8928  xpdom2g  9057  findcard2  9145  unfi  9151  ssfi  9153  fnfi  9158  fodomfi  9268  finsschain  9312  marypha1lem  9389  marypha1  9390  supeq1  9401  ordiso2  9473  ordtypelem7  9482  wemaplem1  9504  inf3lem2  9594  inf3lem5  9597  infdiffi  9623  cantnfval2  9634  cantnfle  9636  cantnfp1lem3  9645  oemapval  9648  cantnflem1  9654  cantnf  9658  wemapwe  9662  cnfcom  9665  cnfcom3clem  9670  ttrclss  9685  ttrclselem2  9691  tz9.1  9694  frr3g  9724  frr2  9728  r1pwALT  9814  cplem2  9872  karden  9877  updjud  9916  infxpenc2lem2  10000  fseqenlem1  10004  dfac8clem  10012  alephinit  10075  dfac4  10102  dfac5lem5  10107  dfac2a  10109  dfac2b  10110  dfacacn  10121  dfac12lem3  10125  kmlem2  10131  kmlem13  10142  nnadju  10177  ackbij1lem16  10213  sornom  10257  infpssrlem4  10286  fin23lem14  10313  fin23lem32  10324  fin23lem34  10326  fin23lem36  10328  isf32lem1  10333  isf32lem2  10334  axcc2lem  10416  axcc3  10418  axcclem  10437  zornn0g  10485  ttukeylem5  10493  ttukeylem6  10494  axrepnd  10575  axpowndlem3  10580  zfcndrep  10595  fpwwe2lem7  10618  pwfseqlem3  10641  wunr1om  10700  wunfi  10702  tskr1om  10748  ingru  10796  grudomon  10798  axgroth3  10812  axgroth4  10813  nqereu  10910  mulcanenq  10941  elnp  10968  elnpi  10969  prlem934  11014  infm3  12170  nnindd  12249  nnaddcl  12252  nnmulcl  12253  nnaddcom  12256  nnne0  12266  nnadddir  12288  nnmulcom  12290  peano5uzi  12681  uzind2  12685  nn0indd  12689  zindd  12693  fzindd  12694  uzaddcl  12924  uzwo  12931  indstr  12936  zmax  12965  xmulasslem  13307  xrsupsslem  13329  xrinfmsslem  13330  xrsupss  13331  xrinfmss  13332  flval2  13843  om2uzlti  13982  uzrdgfni  13990  rabssnn0fi  14018  mptnn0fsupp  14029  seqcl2  14052  seqfveq2  14056  seqshft2  14060  monoord  14064  seqsplit  14067  seqcaopr3  14069  seqf1olem2a  14072  seqf1o  14075  seqid2  14080  seqhomo  14081  ser1const  14090  expcllem  14104  expeq0  14124  mulexp  14133  expadd  14136  expmul  14139  expmordi  14199  leexp2r  14206  leexp1a  14207  bernneq  14261  modexp  14270  facdiv  14319  faclbnd  14322  faclbnd4lem4  14328  hashgadd  14409  hashxp  14467  hashmap  14468  hashf1lem2  14489  hashf1  14490  seqcoll  14497  wrdind  14755  wrd2ind  14756  pfxccatin12lem3  14765  cshweqrep  14854  2cshwcshw  14858  relexp0g  15055  relexpsucnnr  15058  relexpsucnnl  15063  relexpcnv  15068  relexpnndm  15074  relexpaddnn  15084  rtrclreclem1  15090  dfrtrclrec2  15091  rtrclreclem2  15092  rtrclreclem4  15094  dfrtrcl2  15095  relexpind  15097  reusq0  15512  rlim  15542  rlim2  15543  rlim0  15555  rlim0lt  15556  rlimi  15560  ello12r  15564  ello1mpt  15568  ello1d  15570  elo12r  15575  lo1o1  15579  o1lo1  15584  lo1res  15606  climshft  15623  o1compt  15634  rlimo1  15664  lo1add  15674  lo1mul  15675  rlimdiv  15693  climub  15709  climserle  15710  caucvgrlem  15720  caurcvgr  15721  iseraltlem2  15730  summolem2a  15762  sumss  15771  fsum2d  15818  fsumabs  15849  fsumrlim  15859  fsumo1  15860  fsumiun  15869  binom  15880  climcndslem1  15899  climcndslem2  15900  cvgrat  15933  clim2prod  15938  prodfn0  15944  prodfrec  15945  ntrivcvgfvn0  15949  prodmolem2a  15984  fprodabs  16024  fprodn0  16029  fprod2d  16031  binomfallfac  16091  bpolycl  16102  bpolydif  16105  fprodefsum  16145  demoivreALT  16253  ruclem8  16289  ruclem9  16290  dvdsle  16364  dvdsfac  16380  divalglem7  16453  bitsinv1  16496  sadcadd  16512  sadadd2  16514  saddisjlem  16518  smuval2  16536  smupvallem  16537  smu01lem  16539  smupval  16542  smueqlem  16544  smumullem  16546  bezoutlem4  16596  dfgcd2  16600  rplpwr  16612  nn0seqcvgd  16624  seq1st  16625  alginv  16629  algcvga  16633  algfx  16634  lcmf  16687  prmind2  16739  prmdvdsexp  16770  prmfac1  16775  reumodprminv  16860  pcmpt  16948  pcfac  16955  prmpwdvds  16960  prmreclem4  16975  vdwlem10  17046  ramval  17064  ramcl  17085  cshwrepswhash1  17158  prmlem1a  17162  imasleval  17591  ismre  17638  mreexexd  17700  lubprop  18408  lublecllem  18410  glbprop  18421  joinlem  18433  meetlem  18447  poslubmo  18461  posglbmo  18462  poslubd  18463  isglbd  18561  lubun  18567  mndind  18883  frmdgsum  18917  mulgnnass  19171  mhmmulg  19177  gsumwrev  19432  gsmsymgrfix  19494  gsmsymgreq  19498  psgnunilem3  19562  sylow1lem1  19664  efginvrel2  19793  efgsrel  19800  efgredlemd  19810  efgredlem  19813  efgred  19814  efgrelexlemb  19816  gsum2dlem2  20037  gsumcom2  20041  ablfac1eulem  20140  pgpfac1lem2  20143  pgpfac1lem5  20147  pgpfac1  20148  pgpfac  20152  isomnd  20189  omndadd  20194  srgmulgass  20295  srgpcomp  20296  srgbinom  20309  isdomn3  20795  isorng  20938  lmodvsmmulgdi  20992  cnfldexp  21520  ofldchr  21691  islindf4  21953  assamulgscm  22016  mplcoe1  22153  mplcoe3  22154  mplcoe5  22156  gsummoncoe1  22433  dmatval  22614  dmatel  22615  dmatmulcl  22622  pmatcoe1fsupp  22823  decpmataa0  22890  decpmatmulsumfsupp  22895  pmatcollpw2lem  22899  pm2mpmhmlem1  22940  fiinopn  23023  mretopd  23214  neiptoptop  23253  cnpfval  23356  iscnp3  23366  tgcn  23374  lmbr  23380  lmbr2  23381  lmbrf  23382  lmss  23420  ishaus  23444  hausnei2  23475  t1sep2  23491  fiuncmp  23526  dfconn2  23541  1stcfb  23567  2ndc1stc  23573  1stcrest  23575  1stcelcls  23583  1stccn  23585  lly1stc  23618  elkgen  23658  kgencn  23678  tx1stc  23772  xkopt  23777  cnmptcom  23800  isr0  23859  r0sep  23870  ptcmpfi  23935  isfildlem  23979  rnelfm  24075  fbflim  24098  flimrest  24105  isflf  24115  flffbas  24117  lmflf  24127  fclsrest  24146  isfcf  24156  cnextfvval  24187  tmdgsum  24217  eltsms  24255  tsmsi  24256  tsmsgsum  24261  tsmssubm  24265  tsmsres  24266  tsmsf1o  24267  isust  24326  isucn  24399  isucn2  24400  ucnima  24402  imasdsf1olem  24495  metss  24630  met1stc  24643  metcnp  24663  metcnpi  24666  metcnpi2  24667  metucn  24693  xrge0tsms  24957  fsumcn  24994  elcncf  25013  cncfi  25018  rescncf  25021  cncfco  25031  caucfil  25407  equivcau  25424  caubl  25432  caublcls  25433  ovolgelb  25604  ovolunlem1a  25620  ovolicc2lem3  25643  voliunlem1  25674  voliunlem3  25676  volsuplem  25679  volsup  25680  dyadmax  25722  vitali  25737  itg2leub  25858  itgfsum  25951  dvnadd  26053  dvnres  26055  cpnord  26059  dvnfre  26076  dvmptfsum  26099  dvferm1  26109  dvferm2  26111  rolle  26114  dvlip  26117  c1lip1  26121  lhop1  26138  deg1leb  26217  ply1divex  26259  fta1g  26292  plyco  26363  dgrcolem1  26395  dgrco  26397  dvnply2  26413  plydivex  26423  aalioulem2  26459  aalioulem3  26460  aalioulem5  26462  aaliou3lem2  26469  dvntaylp  26496  taylthlem1  26498  ulmdvlem3  26527  abelthlem9  26565  cxpmul2  26816  scvxcvx  27112  jensenlem2  27114  jensen  27115  wilthlem3  27196  perfectlem2  27356  bcmono  27403  bposlem5  27414  lgsquad2lem2  27511  addsq2reu  27566  2sqreulem1  27572  2sqreunnlem1  27575  dchrisumlem1  27615  dchrisum0flb  27636  pntpbnd1  27712  pntlemf  27731  qabvle  27751  qabvexp  27752  ostthlem2  27754  ostth2lem2  27760  nosupcbv  27828  nosupno  27829  nosupdm  27830  nosupfv  27832  nosupres  27833  nosupbnd1lem1  27834  nosupbnd1lem3  27836  nosupbnd1lem5  27838  noinfcbv  27843  noinfno  27844  noinfdm  27845  noinffv  27847  noinfres  27848  noinfbnd1lem3  27851  noinfbnd1lem5  27853  eqcuts2  27941  addsproplem1  28124  addsprop  28131  negsunif  28210  mulsproplem9  28279  sltmuls2  28303  precsexlem8  28369  precsexlem9  28370  precsexlem11  28372  noseqind  28447  om2noseqrdg  28459  noseqrdgfn  28461  n0addscl  28499  n0mulscl  28500  eucliddivs  28531  peano5uzs  28559  expscllem  28585  expadds  28590  expsne0  28591  expsgt0  28592  pw2cut  28615  pw2cut2  28617  bdaypw2n0bnd  28619  tgcgr4  28762  usgr2pth  30050  wlkiswwlks2lem4  30158  wlkiswwlks2  30161  rusgrnumwwlk  30264  clwlkclwwlklem2a  30286  clwlkclwwlklem1  30287  clwlkclwwlkfo  30297  eupth2  30527  frgr3vlem1  30561  3vfriswmgrlem  30565  3vfriswmgr  30566  wlkl0  30655  numclwlk2lem2f1o  30667  isplig  30765  isnvlem  30899  nvi  30903  nmoubi  31061  nmounbi  31065  nmblolbi  31089  ipasslem1  31120  ipassi  31130  hlim2  31481  pjhth  31682  spansni  31846  elspansn2  31856  pjige0  31980  pjcjt2  31981  pjopyth  32009  elcnop  32146  elcnfn  32171  nmopub  32197  cnopc  32202  nmfnleub  32214  elnlfn  32217  cnfnc  32219  nmbdoplb  32314  nmcexi  32315  nmcoplb  32319  lnfnmul  32337  nmbdfnlb  32339  nmcfnlb  32343  pjss2coi  32453  pjssmi  32454  isst  32502  ishst  32503  stcltr1i  32563  mdbr  32583  dmdbr  32588  mddmd2  32598  mdslmd1lem3  32616  mdslmd1lem4  32617  elat2  32629  atcvat2  32678  cdj1i  32722  iuninc  32842  fmptcof2  32939  nn0min  33102  nexple  33114  wrdt2ind  33210  ismnt  33240  xrge0tsmsd  33330  gsumwun  33333  cyc3genpm  33409  isarchi2  33442  archirng  33445  archiexdiv  33447  archiabl  33455  domnprodn0  33535  islbs5  33633  unitprodclb  33642  mxidlval  33685  1arithidom  33768  1arithufdlem3  33777  crefeq  34176  esumfzf  34400  issiga  34443  isrnsiga  34444  isldsys  34487  ismeas  34530  isrnmeas  34531  measiun  34549  eulerpartlemn  34712  sseqp1  34726  rrvsum  34785  signsply0  34879  signstfvc  34902  bnj941  35102  bnj106  35197  bnj155  35208  bnj590  35239  bnj591  35240  bnj849  35254  bnj893  35257  bnj944  35267  bnj1128  35319  r1filimi  35435  r1omhfb  35444  tz9.1regs  35466  r1omhfbregs  35469  gblacfnacd  35481  subfacp1lem6  35572  erdszelem8  35585  issconn  35613  cvmliftlem7  35678  cvmliftlem10  35681  cvmlift3lem2  35707  satfsschain  35751  satfrel  35754  satfdm  35756  satfrnmapom  35757  fmlafvel  35772  satffun  35796  mrsubvrs  35909  mclsssvlem  35949  mclsval  35950  mclsax  35956  mclsind  35957  shftvalg  36119  bccolsum  36126  iprodefisumlem  36127  faclimlem1  36130  rdgprc  36179  sbequbidv  36611  cbvsbdavw  36651  fveleq  36847  dfttc4lem1  36924  dfttc4  36926  elttcirr  36927  regsfromregtco  36934  mh-unprimbi  36940  unblimceq0  36981  bj-ax12  37164  bj-bm1.3ii  37584  rdgeqoa  37899  finxpreclem6  37925  domalom  37933  ralssiun  37936  wl-ax12v2cl  38035  wl-sblimt  38086  wl-sbhbt  38092  wl-2sb6d  38096  wl-mo2df  38108  wl-mo2t  38113  poimirlem2  38156  poimirlem25  38179  poimirlem28  38182  poimirlem31  38185  heicant  38189  mbfresfi  38200  itg2gt0cn  38209  sdclem2  38276  fdc  38279  seqpo  38281  incsequz  38282  mettrifi  38291  prdsbnd2  38329  heiborlem4  38348  bfplem1  38356  iscringd  38532  maxidlval  38573  igenval2  38600  iss2  38878  elrefrels3  39133  ax12eq  39600  ax12el  39601  ax12indalem  39604  ax12inda2ALT  39605  ax12inda  39607  ax12v2-o  39608  riotasvd  39615  isopos  39839  isat3  39966  ishlat1  40011  glbconN  40036  ispsubsp  40404  isldil  40769  isltrn  40778  isdilN  40813  trlval  40821  cdleme27b  41027  cdleme29b  41034  cdleme31sn1  41040  cdleme31sn1c  41047  cdleme40v  41128  cdlemk36  41572  cdlemkid5  41594  cdlemn11pre  41869  dihord2pre  41884  islpolN  42142  hdmapffval  42485  hdmapfval  42486  hdmapval2lem  42490  uzindd  42630  sticksstones1  42798  sticksstones2  42799  sticksstones3  42800  sticksstones8  42805  sticksstones10  42807  sticksstones11  42808  sticksstones12a  42809  sticksstones15  42813  indstrd  42845  unitscyglem3  42849  eu6w  43295  ismrc  43319  incssnn0  43329  mzpexpmpt  43363  pell14qrexpclnn0  43480  monotuz  43555  rmxypos  43561  jm2.17a  43574  jm2.17b  43575  rmygeid  43578  jm2.18  43602  jm2.19lem3  43605  jm2.25  43613  jm2.15nn0  43617  jm2.16nn0  43618  wepwsolem  43656  aomclem8  43675  dfac11  43676  pwslnm  43708  lnr2i  43730  hbtlem5  43742  cnsrexpcl  43779  rngunsnply  43783  unielss  43832  onsucf1lem  43883  cantnfresb  43938  onmcl  43945  naddonnn  44009  elmapintrab  44189  elmapintab  44209  cnvcnvintabd  44213  eliunov2  44292  relexpxpnnidm  44316  relexpiidm  44317  relexpss1d  44318  iunrelexpmin1  44321  relexpmulnn  44322  iunrelexpmin2  44325  relexp0a  44329  trclimalb2  44339  clsk3nimkb  44653  ntrclsiso  44680  ntrclskb  44682  ntrneiiso  44704  ntrneix2  44706  ntrneixb  44708  gneispace2  44745  gneispacess2  44759  mnuunid  44874  dvgrat  44909  pm14.122b  45020  relpeq1  45540  relpeq3  45542  trfr  45558  pwclaxpow  45580  prclaxpr  45581  uniclaxun  45582  modelac8prim  45588  permaxpow  45605  permaxpr  45606  permaxun  45607  nregmodel  45613  fnchoice  45636  fiiuncl  45672  ssinc  45692  ssdec  45693  wessf1ornlem  45790  dmrelrnrel  45829  fperiodmullem  45909  monoordxrv  46082  fmul01  46183  fmuldfeq  46186  climsuselem1  46210  climinff  46214  ellimcabssub0  46220  limcleqr  46245  addlimc  46249  0ellimcdiv  46250  limclner  46252  limsupref  46286  limsupub  46305  limsupmnf  46322  limsupre2lem  46325  limsupre2  46326  limsupre2mpt  46331  limsupre3lem  46333  limsupre3  46334  limsupre3mpt  46335  xlimbr  46428  cnrefiisplem  46430  dvnmptdivc  46539  dvnmptconst  46542  dvnmul  46544  iblspltprt  46574  itgspltprt  46580  stoweidlem2  46603  stoweidlem3  46604  stoweidlem17  46618  stoweidlem19  46620  stoweidlem21  46622  stoweidlem26  46627  fourierdlem42  46750  issal  46915  ismea  47052  isome  47095  carageniuncllem1  47122  caratheodorylem1  47127  2reu8i  47734  2reuimp0  47735  funressndmafv2rn  47844  2ffzoeq  47949  smonoord  47998  fargshiftf1  48074  ichnfimlem  48096  paireqne  48144  reupr  48155  reuopreuprim  48159  perfectALTVlem2  48371  grimcnv  48537  pgnbgreunbgrlem1  48762  pgnbgreunbgrlem4  48768  pgnbgreunbgr  48774  lmodvsmdi  49039  dmatALTval  49060  dmatALTbasel  49062  snlindsntor  49131  ldepsnlinc  49168  elbigo2r  49213  elbigolo1  49217  itcovalt2  49337  mof0  49496  isnrm4  49589  iscnrm3r  49606  iscnrm4  49612  lubsscl  49618  glbsscl  49619  ipolubdm  49645  ipoglbdm  49648  setrecseq  50343  setrec2fun  50350  setrec2lem2  50352