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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  imbi12d  347  imbi2  351  pm5.42  546  orbi2d  912  con3ALTOLD  1081  19.23t  2210  axc14  2486  mojust  2621  mof  2647  eu6lem  2658  nfabdw  3000  2gencl  3535  3gencl  3536  vtocl2gf  3570  vtocl3gf  3571  vtocl2g  3572  vtocl2ga  3575  vtocl4g  3579  eqeu  3697  mo2icl  3705  euind  3715  reu7  3723  reuind  3744  sbctt  3844  reu8nf  3860  vtocl2dOLD  3931  sbcnestgfw  4370  sbcnestgf  4375  r19.36zv  4452  dedth2h  4524  dedth3h  4525  dedth4h  4526  reusngf  4612  reuprg0  4638  preq12bg  4784  elint  4882  elintrabg  4889  intab  4906  axrep1  5191  axreplem  5192  axrep2  5193  bm1.3ii  5206  reusv3  5306  pocl  5481  swopolem  5483  solin  5498  freq1  5525  frminex  5535  vtoclr  5615  2optocl  5646  3optocl  5647  raliunxp  5710  resieq  5864  iss  5903  cnveqb  6053  reu3op  6143  reuop  6144  preddowncl  6175  funmo  6371  funimaexg  6440  fnbrfvb  6718  fvelimab  6737  fvmptss  6780  fmptco  6891  fprg  6917  fnressn  6920  fressnfv  6922  isoselem  7094  ovg  7313  caovcan  7352  caovordig  7353  caovord  7359  tfisi  7573  tfindsg  7575  tfinds2  7578  tfinds3  7579  dfom2  7582  elom  7583  findsg  7609  finds2  7610  f1o2ndf1  7818  poxp  7822  fnse  7827  wfr3g  7953  wfrlem4  7958  smoeq  7987  smores  7989  smogt  8004  tfrlem1  8012  tfr3  8035  oaordi  8172  oeordi  8213  oeoa  8223  oeoe  8225  nnacl  8237  nnmcl  8238  nnecl  8239  nnacom  8243  nnaordi  8244  nnawordi  8247  nnaass  8248  nndi  8249  nnmass  8250  nnmsucr  8251  nnmcom  8252  nnmordi  8257  2ecoptocl  8388  3ecoptocl  8389  undifixp  8498  xpdom2g  8613  findcard2  8758  xpfi  8789  fnfi  8796  fodomfi  8797  finsschain  8831  marypha1lem  8897  marypha1  8898  supeq1  8909  ordiso2  8979  ordtypelem7  8988  wemaplem1  9010  inf3lem2  9092  inf3lem5  9095  infdiffi  9121  cantnfval2  9132  cantnfle  9134  cantnfp1lem3  9143  oemapval  9146  cantnflem1  9152  cantnf  9156  wemapwe  9160  cnfcom  9163  cnfcom3clem  9168  tz9.1  9171  r1pwALT  9275  cplem2  9319  karden  9324  updjud  9363  infxpenc2lem2  9446  fseqenlem1  9450  dfac8clem  9458  alephinit  9521  dfac4  9548  dfac5lem5  9553  dfac2a  9555  dfac2b  9556  dfacacn  9567  dfac12lem3  9571  kmlem2  9577  kmlem13  9588  ackbij1lem16  9657  sornom  9699  infpssrlem4  9728  fin23lem14  9755  fin23lem32  9766  fin23lem34  9768  fin23lem36  9770  isf32lem1  9775  isf32lem2  9776  axcc2lem  9858  axcc3  9860  axcclem  9879  zornn0g  9927  ttukeylem5  9935  ttukeylem6  9936  axrepnd  10016  axpowndlem3  10021  zfcndrep  10036  fpwwe2lem8  10059  pwfseqlem3  10082  wunr1om  10141  wunfi  10143  tskr1om  10189  ingru  10237  grudomon  10239  axgroth3  10253  axgroth4  10254  nqereu  10351  mulcanenq  10382  elnp  10409  elnpi  10410  prlem934  10455  infm3  11600  nnindd  11658  nnaddcl  11661  nnmulcl  11662  nnne0  11672  peano5uzi  12072  uzind2  12076  nn0indd  12080  zindd  12084  eluzadd  12274  uzaddcl  12305  uzwo  12312  indstr  12317  zmax  12346  xmulasslem  12679  xrsupsslem  12701  xrinfmsslem  12702  xrsupss  12703  xrinfmss  12704  flval2  13185  om2uzlti  13319  uzrdgfni  13327  rabssnn0fi  13355  mptnn0fsupp  13366  seqcl2  13389  seqfveq2  13393  seqshft2  13397  monoord  13401  seqsplit  13404  seqcaopr3  13406  seqf1olem2a  13409  seqf1o  13412  seqid2  13417  seqhomo  13418  ser1const  13427  expcllem  13441  expeq0  13460  mulexp  13469  expadd  13472  expmul  13475  expmordi  13532  leexp2r  13539  leexp1a  13540  bernneq  13591  modexp  13600  facdiv  13648  faclbnd  13651  faclbnd4lem4  13657  hashgadd  13739  hashxp  13796  hashmap  13797  hashf1lem2  13815  hashf1  13816  seqcoll  13823  wrdind  14084  wrd2ind  14085  pfxccatin12lem3  14094  cshweqrep  14183  2cshwcshw  14187  relexp0g  14381  relexpsucnnr  14384  relexpsucnnl  14391  relexpcnv  14394  relexpnndm  14400  relexpaddnn  14410  dfrtrclrec2  14416  rtrclreclem1  14417  rtrclreclem2  14418  rtrclreclem4  14420  dfrtrcl2  14421  relexpind  14423  reusq0  14822  rlim  14852  rlim2  14853  rlim0  14865  rlim0lt  14866  rlimi  14870  ello12r  14874  ello1mpt  14878  ello1d  14880  elo12r  14885  lo1o1  14889  o1lo1  14894  lo1res  14916  climshft  14933  o1compt  14944  rlimo1  14973  lo1add  14983  lo1mul  14984  rlimdiv  15002  climub  15018  climserle  15019  caucvgrlem  15029  caurcvgr  15030  iseraltlem2  15039  summolem2a  15072  sumss  15081  fsum2d  15126  fsumabs  15156  fsumrlim  15166  fsumo1  15167  fsumiun  15176  binom  15185  climcndslem1  15204  climcndslem2  15205  cvgrat  15239  clim2prod  15244  prodfn0  15250  prodfrec  15251  ntrivcvgfvn0  15255  prodmolem2a  15288  fprodabs  15328  fprodn0  15333  fprod2d  15335  binomfallfac  15395  bpolycl  15406  bpolydif  15409  fprodefsum  15448  demoivreALT  15554  ruclem8  15590  ruclem9  15591  dvdsle  15660  dvdsfac  15676  divalglem7  15750  bitsinv1  15791  sadcadd  15807  sadadd2  15809  saddisjlem  15813  smuval2  15831  smupvallem  15832  smu01lem  15834  smupval  15837  smueqlem  15839  smumullem  15841  bezoutlem4  15890  dfgcd2  15894  gcdmultipleOLD  15900  rplpwr  15907  nn0seqcvgd  15914  seq1st  15915  alginv  15919  algcvga  15923  algfx  15924  lcmf  15977  prmind2  16029  prmdvdsexp  16059  prmfac1  16063  reumodprminv  16141  pcmpt  16228  pcfac  16235  prmpwdvds  16240  prmreclem4  16255  vdwlem10  16326  ramval  16344  ramcl  16365  cshwrepswhash1  16436  prmlem1a  16440  imasleval  16814  ismre  16861  mreexexd  16919  lubprop  17596  lublecllem  17598  glbprop  17609  joinlem  17621  meetlem  17635  isglbd  17727  lubun  17733  poslubmo  17756  posglbmo  17757  poslubd  17758  mndind  17992  frmdgsum  18027  mulgnnass  18262  mhmmulg  18268  gsumwrev  18494  gsmsymgrfix  18556  gsmsymgreq  18560  psgnunilem3  18624  sylow1lem1  18723  efginvrel2  18853  efgsrel  18860  efgredlemd  18870  efgredlem  18873  efgred  18874  efgrelexlemb  18876  gsum2dlem2  19091  gsumcom2  19095  ablfac1eulem  19194  pgpfac1lem2  19197  pgpfac1lem5  19201  pgpfac1  19202  pgpfac  19206  srgmulgass  19281  srgpcomp  19282  srgbinom  19295  lmodvsmmulgdi  19669  isdomn2  20072  assamulgscm  20130  mplcoe1  20246  mplcoe3  20247  mplcoe5  20249  gsummoncoe1  20472  cnfldexp  20578  islindf4  20982  dmatval  21101  dmatel  21102  dmatmulcl  21109  pmatcoe1fsupp  21309  decpmataa0  21376  decpmatmulsumfsupp  21381  pmatcollpw2lem  21385  pm2mpmhmlem1  21426  fiinopn  21509  mretopd  21700  neiptoptop  21739  cnpfval  21842  iscnp3  21852  tgcn  21860  lmbr  21866  lmbr2  21867  lmbrf  21868  lmss  21906  ishaus  21930  hausnei2  21961  t1sep2  21977  fiuncmp  22012  dfconn2  22027  1stcfb  22053  2ndc1stc  22059  1stcrest  22061  1stcelcls  22069  1stccn  22071  lly1stc  22104  elkgen  22144  kgencn  22164  tx1stc  22258  xkopt  22263  cnmptcom  22286  isr0  22345  r0sep  22356  ptcmpfi  22421  isfildlem  22465  rnelfm  22561  fbflim  22584  flimrest  22591  isflf  22601  flffbas  22603  lmflf  22613  fclsrest  22632  isfcf  22642  cnextfvval  22673  tmdgsum  22703  eltsms  22741  tsmsi  22742  tsmsgsum  22747  tsmssubm  22751  tsmsres  22752  tsmsf1o  22753  isust  22812  isucn  22887  isucn2  22888  ucnima  22890  imasdsf1olem  22983  metss  23118  met1stc  23131  metcnp  23151  metcnpi  23154  metcnpi2  23155  metucn  23181  xrge0tsms  23442  fsumcn  23478  elcncf  23497  cncfi  23502  rescncf  23505  cncfco  23515  caucfil  23886  equivcau  23903  caubl  23911  caublcls  23912  ovolgelb  24081  ovolunlem1a  24097  ovolicc2lem3  24120  voliunlem1  24151  voliunlem3  24153  volsuplem  24156  volsup  24157  dyadmax  24199  vitali  24214  itg2leub  24335  itgfsum  24427  dvnadd  24526  dvnres  24528  cpnord  24532  dvnfre  24549  dvmptfsum  24572  dvferm1  24582  dvferm2  24584  rolle  24587  dvlip  24590  c1lip1  24594  lhop1  24611  deg1leb  24689  ply1divex  24730  fta1g  24761  plyco  24831  dgrcolem1  24863  dgrco  24865  dvnply2  24876  plydivex  24886  aalioulem2  24922  aalioulem3  24923  aalioulem5  24925  aaliou3lem2  24932  dvntaylp  24959  taylthlem1  24961  ulmdvlem3  24990  abelthlem9  25028  cxpmul2  25272  scvxcvx  25563  jensenlem2  25565  jensen  25566  wilthlem3  25647  perfectlem2  25806  bcmono  25853  bposlem5  25864  lgsquad2lem2  25961  addsq2reu  26016  2sqreulem1  26022  2sqreunnlem1  26025  dchrisumlem1  26065  dchrisum0flb  26086  pntpbnd1  26162  pntlemf  26181  qabvle  26201  qabvexp  26202  ostthlem2  26204  ostth2lem2  26210  tgcgr4  26317  usgr2pth  27545  wlkiswwlks2lem4  27650  wlkiswwlks2  27653  rusgrnumwwlk  27754  clwlkclwwlklem2a  27776  clwlkclwwlklem1  27777  clwlkclwwlkfo  27787  eupth2  28018  frgr3vlem1  28052  3vfriswmgrlem  28056  3vfriswmgr  28057  wlkl0  28146  numclwlk2lem2f1o  28158  isplig  28253  isnvlem  28387  nvi  28391  nmoubi  28549  nmounbi  28553  nmblolbi  28577  ipasslem1  28608  ipassi  28618  hlim2  28969  pjhth  29170  spansni  29334  elspansn2  29344  pjige0  29468  pjcjt2  29469  pjopyth  29497  elcnop  29634  elcnfn  29659  nmopub  29685  cnopc  29690  nmfnleub  29702  elnlfn  29705  cnfnc  29707  nmbdoplb  29802  nmcexi  29803  nmcoplb  29807  lnfnmul  29825  nmbdfnlb  29827  nmcfnlb  29831  pjss2coi  29941  pjssmi  29942  isst  29990  ishst  29991  stcltr1i  30051  mdbr  30071  dmdbr  30076  mddmd2  30086  mdslmd1lem3  30104  mdslmd1lem4  30105  elat2  30117  atcvat2  30166  cdj1i  30210  iuninc  30312  fmptcof2  30402  nn0min  30536  wrdt2ind  30627  xrge0tsmsd  30692  isomnd  30702  omndadd  30707  cyc3genpm  30794  isarchi2  30814  archirng  30817  archiexdiv  30819  archiabl  30827  isorng  30872  ofldchr  30887  mxidlval  30970  crefeq  31109  nexple  31268  esumfzf  31328  issiga  31371  isrnsiga  31372  isldsys  31415  ismeas  31458  isrnmeas  31459  measiun  31477  eulerpartlemn  31639  sseqp1  31653  rrvsum  31712  signsply0  31821  signstfvc  31844  bnj941  32044  bnj106  32140  bnj155  32151  bnj590  32182  bnj591  32183  bnj849  32197  bnj893  32200  bnj944  32210  bnj1128  32262  subfacp1lem6  32432  erdszelem8  32445  issconn  32473  cvmliftlem7  32538  cvmliftlem10  32541  cvmlift3lem2  32567  satfsschain  32611  satfrel  32614  satfdm  32616  satfrnmapom  32617  fmlafvel  32632  satffun  32656  mrsubvrs  32769  mclsssvlem  32809  mclsval  32810  mclsax  32816  mclsind  32817  shftvalg  32963  bccolsum  32971  iprodefisumlem  32972  faclimlem1  32975  dfpo2  32991  rdgprc  33039  trpredmintr  33070  frmin  33084  soseq  33096  frr3g  33121  fpr3g  33122  frrlem12  33134  fpr2  33140  frr2  33145  nosupno  33203  nosupdm  33204  nosupfv  33206  nosupres  33207  nosupbnd1lem1  33208  nosupbnd1lem3  33210  nosupbnd1lem5  33212  noeta  33222  fveleq  33799  unblimceq0  33846  bj-ax12  33990  bj-bm1.3ii  34360  rdgeqoa  34654  finxpreclem6  34680  domalom  34688  ralssiun  34691  wl-sblimt  34802  wl-sbhbt  34805  wl-2sb6d  34809  wl-mo2df  34821  wl-mo2t  34826  poimirlem2  34909  poimirlem25  34932  poimirlem28  34935  poimirlem31  34938  heicant  34942  mbfresfi  34953  itg2gt0cn  34962  sdclem2  35032  fdc  35035  seqpo  35037  incsequz  35038  mettrifi  35047  prdsbnd2  35088  heiborlem4  35107  bfplem1  35115  iscringd  35291  maxidlval  35332  igenval2  35359  iss2  35616  elrefrels3  35773  ax12eq  36092  ax12el  36093  ax12indalem  36096  ax12inda2ALT  36097  ax12inda  36099  ax12v2-o  36100  riotasvd  36107  isopos  36331  isat3  36458  ishlat1  36503  glbconN  36528  ispsubsp  36896  isldil  37261  isltrn  37270  isdilN  37305  trlval  37313  cdleme27b  37519  cdleme29b  37526  cdleme31sn1  37532  cdleme31sn1c  37539  cdleme40v  37620  cdlemk36  38064  cdlemkid5  38086  cdlemn11pre  38361  dihord2pre  38376  islpolN  38634  hdmapffval  38977  hdmapfval  38978  hdmapval2lem  38982  nnaddcom  39181  nnadddir  39183  nnmulcom  39185  ismrc  39318  incssnn0  39328  mzpexpmpt  39362  pell14qrexpclnn0  39483  monotuz  39558  rmxypos  39564  jm2.17a  39577  jm2.17b  39578  rmygeid  39581  jm2.18  39605  jm2.19lem3  39608  jm2.25  39616  jm2.15nn0  39620  jm2.16nn0  39621  wepwsolem  39662  aomclem8  39681  dfac11  39682  pwslnm  39714  lnr2i  39736  hbtlem5  39748  cnsrexpcl  39785  rngunsnply  39793  isdomn3  39824  ifpbi23  39858  elmapintrab  39956  elmapintab  39976  cnvcnvintabd  39980  eliunov2  40044  relexpxpnnidm  40068  relexpiidm  40069  relexpss1d  40070  iunrelexpmin1  40073  relexpmulnn  40074  iunrelexpmin2  40077  relexp0a  40081  trclimalb2  40091  clsk3nimkb  40410  ntrclsiso  40437  ntrclskb  40439  ntrneiiso  40461  ntrneix2  40463  ntrneixb  40465  gneispace2  40502  gneispacess2  40516  mnuunid  40633  dvgrat  40664  pm14.122b  40775  fnchoice  41306  fiiuncl  41347  ssinc  41373  ssdec  41374  wessf1ornlem  41465  dmrelrnrel  41510  fperiodmullem  41590  monoordxrv  41778  fmul01  41881  fmuldfeq  41884  climsuselem1  41908  climinff  41912  ellimcabssub0  41918  limcleqr  41945  addlimc  41949  0ellimcdiv  41950  limclner  41952  limsupref  41986  limsupub  42005  limsupmnf  42022  limsupre2lem  42025  limsupre2  42026  limsupre2mpt  42031  limsupre3lem  42033  limsupre3  42034  limsupre3mpt  42035  xlimbr  42128  cnrefiisplem  42130  dvnmptdivc  42243  dvnmptconst  42246  dvnmul  42248  iblspltprt  42278  itgspltprt  42284  stoweidlem2  42307  stoweidlem3  42308  stoweidlem17  42322  stoweidlem19  42324  stoweidlem21  42326  stoweidlem26  42331  fourierdlem42  42454  issal  42619  ismea  42753  isome  42796  carageniuncllem1  42823  caratheodorylem1  42828  2reu8i  43332  2reuimp0  43333  funressndmafv2rn  43442  2ffzoeq  43548  smonoord  43551  fargshiftf1  43621  paireqne  43693  reupr  43704  reuopreuprim  43708  perfectALTVlem2  43907  lmodvsmdi  44450  dmatALTval  44475  dmatALTbasel  44477  snlindsntor  44546  ldepsnlinc  44583  elbigo2r  44633  elbigolo1  44637  setrecseq  44808  setrec2fun  44815  setrec2lem2  44817