Theorem imbi2d 330

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  imbi12d  334  imbi2  338  pm5.42  571  orbi2d  738  con3ALT  1032  con3OLD  1035  axc15  2303  ax12v2OLD  2342  axc14  2372  mo2  2479  2gencl  3236  3gencl  3237  vtocl2gf  3268  vtocl3gf  3269  vtocl4g  3277  eqeu  3377  mo2icl  3385  euind  3393  reu7  3401  reuind  3411  sbctt  3500  reu8nf  3516  sbcnestgf  3995  r19.36zv  4072  dedth2h  4140  dedth3h  4141  dedth4h  4142  preq12bg  4386  prel12g  4387  elint  4481  elintrabg  4489  intab  4507  trssOLD  4762  axrep1  4772  axrep2  4773  axrep3  4774  bm1.3ii  4784  reusv3  4876  pocl  5042  swopolem  5044  solin  5058  freq1  5084  frminex  5094  vtoclr  5164  2optocl  5196  3optocl  5197  raliunxp  5261  resieq  5407  iss  5447  cnveqb  5590  preddowncl  5707  funmo  5904  funimaexg  5975  fnbrfvb  6236  fvelimab  6253  fvmptss  6292  fmptco  6396  fprg  6422  fnressn  6425  fressnfv  6427  isoselem  6591  ovg  6799  caovcan  6838  caovordig  6839  caovord  6845  tfisi  7058  tfindsg  7060  tfinds2  7063  tfinds3  7064  dfom2  7067  elom  7068  findsg  7093  finds2  7094  f1o2ndf1  7285  poxp  7289  fnse  7294  wfr3g  7413  wfrlem4  7418  smoeq  7447  smores  7449  smogt  7464  tfrlem1  7472  tfr3  7495  oaordi  7626  oeordi  7667  oeoa  7677  oeoe  7679  nnacl  7691  nnmcl  7692  nnecl  7693  nnacom  7697  nnaordi  7698  nnawordi  7701  nnaass  7702  nndi  7703  nnmass  7704  nnmsucr  7705  nnmcom  7706  nnmordi  7711  2ecoptocl  7838  3ecoptocl  7839  undifixp  7944  xpdom2g  8056  findcard2  8200  xpfi  8231  fnfi  8238  fodomfi  8239  finsschain  8273  marypha1lem  8339  marypha1  8340  supeq1  8351  ordiso2  8420  ordtypelem7  8429  wemaplem1  8451  inf3lem2  8526  inf3lem5  8529  infdiffi  8555  cantnfval2  8566  cantnfle  8568  cantnfp1lem3  8577  oemapval  8580  cantnflem1  8586  cantnf  8590  wemapwe  8594  cnfcom  8597  cnfcom3clem  8602  tz9.1  8605  r1pwALT  8709  cplem2  8753  karden  8758  infxpenc2lem2  8843  fseqenlem1  8847  dfac8clem  8855  alephinit  8918  dfac4  8945  dfac5lem5  8950  dfac2a  8952  dfac2  8953  dfacacn  8963  dfac12lem3  8967  kmlem2  8973  kmlem13  8984  ackbij1lem16  9057  sornom  9099  infpssrlem4  9128  fin23lem14  9155  fin23lem32  9166  fin23lem34  9168  fin23lem36  9170  isf32lem1  9175  isf32lem2  9176  axcc2lem  9258  axcc3  9260  axcclem  9279  zornn0g  9327  ttukeylem5  9335  ttukeylem6  9336  axrepnd  9416  axpowndlem3  9421  zfcndrep  9436  fpwwe2lem8  9459  pwfseqlem3  9482  wunr1om  9541  wunfi  9543  tskr1om  9589  ingru  9637  grudomon  9639  axgroth3  9653  axgroth4  9654  nqereu  9751  mulcanenq  9782  elnp  9809  elnpi  9810  prlem934  9855  infm3  10982  nnaddcl  11042  nnmulcl  11043  peano5uzi  11466  uzind2  11470  nn0indd  11474  zindd  11478  eluzadd  11716  uzaddcl  11744  uzwo  11751  indstr  11756  zmax  11785  xmulasslem  12115  xrsupsslem  12137  xrinfmsslem  12138  xrsupss  12139  xrinfmss  12140  flval2  12615  om2uzlti  12749  uzrdgfni  12757  rabssnn0fi  12785  mptnn0fsupp  12797  seqcl2  12819  seqfveq2  12823  seqshft2  12827  monoord  12831  seqsplit  12834  seqcaopr3  12836  seqf1olem2a  12839  seqf1o  12842  seqid2  12847  seqhomo  12848  ser1const  12857  expcllem  12871  expeq0  12890  mulexp  12899  expadd  12902  expmul  12905  leexp2r  12918  leexp1a  12919  bernneq  12990  modexp  12999  facdiv  13074  faclbnd  13077  faclbnd4lem4  13083  faclbnd6  13086  hashgadd  13166  hashxp  13221  hashmap  13222  hashf1lem2  13240  hashf1  13241  seqcoll  13248  wrdind  13476  wrd2ind  13477  swrdccatin12lem3  13490  cshweqrep  13567  2cshwcshw  13571  relexp0g  13762  relexpsucnnr  13765  relexpsucnnl  13772  relexpcnv  13775  relexpnndm  13781  relexpaddnn  13791  dfrtrclrec2  13797  rtrclreclem1  13798  rtrclreclem2  13799  rtrclreclem4  13801  dfrtrcl2  13802  relexpind  13804  cjexp  13890  absexp  14044  rlim  14226  rlim2  14227  rlim0  14239  rlim0lt  14240  rlimi  14244  ello12r  14248  ello1mpt  14252  ello1d  14254  elo12r  14259  lo1o1  14263  o1lo1  14268  lo1res  14290  climshft  14307  o1compt  14318  rlimo1  14347  lo1add  14357  lo1mul  14358  rlimdiv  14376  climub  14392  climserle  14393  caucvgrlem  14403  caurcvgr  14404  iseraltlem2  14413  summolem2a  14446  sumss  14455  fsum2d  14502  fsumabs  14533  fsumrlim  14543  fsumo1  14544  fsumiun  14553  binom  14562  bcxmas  14567  climcndslem1  14581  climcndslem2  14582  cvgrat  14615  clim2prod  14620  prodfn0  14626  prodfrec  14627  ntrivcvgfvn0  14631  prodmolem2a  14664  fprodabs  14704  fprodn0  14709  fprod2d  14711  binomfallfac  14772  bpolycl  14783  bpolydif  14786  fprodefsum  14825  demoivreALT  14931  ruclem8  14966  ruclem9  14967  dvdsle  15032  dvdsfac  15048  divalglem7  15122  bitsinv1  15164  sadcadd  15180  sadadd2  15182  saddisjlem  15186  smuval2  15204  smupvallem  15205  smu01lem  15207  smupval  15210  smueqlem  15212  smumullem  15214  bezoutlem4  15259  dfgcd2  15263  gcdmultiple  15269  rplpwr  15276  nn0seqcvgd  15283  seq1st  15284  alginv  15288  algcvga  15292  algfx  15293  lcmf  15346  prmind2  15398  prmdvdsexp  15427  prmfac1  15431  reumodprminv  15509  pcmpt  15596  pcfac  15603  prmpwdvds  15608  prmreclem4  15623  vdwlem10  15694  ramval  15712  ramcl  15733  cshwrepswhash1  15809  prmlem1a  15813  imasleval  16201  ismre  16250  mreexexd  16308  mreexexdOLD  16309  lubprop  16986  lublecllem  16988  glbprop  16999  joinlem  17011  meetlem  17025  isglbd  17117  lubun  17123  poslubmo  17146  posglbmo  17147  poslubd  17148  mrcmndind  17366  frmdgsum  17399  mulgnnass  17576  mulgnnassOLD  17577  mhmmulg  17583  gsumwrev  17796  gsmsymgrfix  17848  gsmsymgreq  17852  psgnunilem3  17916  sylow1lem1  18013  efginvrel2  18140  efgsrel  18147  efgredlemd  18157  efgredlem  18160  efgred  18161  efgrelexlemb  18163  gsum2dlem2  18370  gsumcom2  18374  ablfac1eulem  18471  pgpfac1lem2  18474  pgpfac1lem5  18478  pgpfac1  18479  pgpfac  18483  srgmulgass  18531  srgpcomp  18532  srgbinom  18545  lmodvsmmulgdi  18898  isdomn2  19299  assamulgscm  19350  mplcoe1  19465  mplcoe3  19466  mplcoe5  19468  gsummoncoe1  19674  cnfldexp  19779  islindf4  20177  dmatval  20298  dmatel  20299  dmatmulcl  20306  pmatcoe1fsupp  20506  decpmataa0  20573  decpmatmulsumfsupp  20578  pmatcollpw2lem  20582  pm2mpmhmlem1  20623  fiinopn  20706  mretopd  20896  neiptoptop  20935  cnpfval  21038  iscnp3  21048  tgcn  21056  lmbr  21062  lmbr2  21063  lmbrf  21064  lmss  21102  ishaus  21126  hausnei2  21157  t1sep2  21173  fiuncmp  21207  dfconn2  21222  1stcfb  21248  2ndc1stc  21254  1stcrest  21256  1stcelcls  21264  1stccn  21266  lly1stc  21299  elkgen  21339  kgencn  21359  tx1stc  21453  xkopt  21458  cnmptcom  21481  isr0  21540  r0sep  21551  ptcmpfi  21616  isfildlem  21661  rnelfm  21757  fbflim  21780  flimrest  21787  isflf  21797  flffbas  21799  lmflf  21809  fclsrest  21828  isfcf  21838  cnextfvval  21869  tmdmulg  21896  tmdgsum  21899  eltsms  21936  tsmsi  21937  tsmsgsum  21942  tsmssubm  21946  tsmsres  21947  tsmsf1o  21948  isust  22007  isucn  22082  isucn2  22083  ucnima  22085  imasdsf1olem  22178  metss  22313  met1stc  22326  metcnp  22346  metcnpi  22349  metcnpi2  22350  metucn  22376  xrge0tsms  22637  fsumcn  22673  elcncf  22692  cncfi  22697  rescncf  22700  cncfco  22710  caucfil  23081  equivcau  23098  caubl  23106  caublcls  23107  ovolgelb  23248  ovolunlem1a  23264  ovolicc2lem3  23287  voliunlem1  23318  voliunlem3  23320  volsuplem  23323  volsup  23324  dyadmax  23366  vitali  23382  itg2leub  23501  itgfsum  23593  dvnadd  23692  dvnres  23694  cpnord  23698  dvnfre  23715  dvmptfsum  23738  dvferm1  23748  dvferm2  23750  rolle  23753  dvlip  23756  c1lip1  23760  lhop1  23777  deg1leb  23855  ply1divex  23896  fta1g  23927  plyco  23997  dgrcolem1  24029  dgrco  24031  dvnply2  24042  plydivex  24052  aalioulem2  24088  aalioulem3  24089  aalioulem5  24091  aaliou3lem2  24098  dvntaylp  24125  taylthlem1  24127  ulmdvlem3  24156  abelthlem9  24194  cxpmul2  24435  scvxcvx  24712  jensenlem2  24714  jensen  24715  wilthlem3  24796  perfectlem2  24955  bcmono  25002  bposlem5  25013  lgsquad2lem2  25110  dchrisumlem1  25178  dchrisum0flb  25199  pntpbnd1  25275  pntlemf  25294  qabvle  25314  qabvexp  25315  ostthlem2  25317  ostth2lem2  25323  tgcgr4  25426  usgr2pth  26660  wlkiswwlks2lem4  26758  wlkiswwlks2  26761  rusgrnumwwlk  26870  clwlkclwwlklem2a  26899  clwlkclwwlklem1  26900  clwlksfoclwwlk  26963  eupth2  27099  frgr3vlem1  27137  3vfriswmgrlem  27141  3vfriswmgr  27142  numclwlk2lem2f1o  27238  isplig  27328  isnvlem  27465  nvi  27469  nmoubi  27627  nmounbi  27631  nmblolbi  27655  ipasslem1  27686  ipassi  27696  hlim2  28049  pjhth  28252  spansni  28416  elspansn2  28426  pjige0  28550  pjcjt2  28551  pjopyth  28579  elcnop  28716  elcnfn  28741  nmopub  28767  cnopc  28772  nmfnleub  28784  elnlfn  28787  cnfnc  28789  nmbdoplb  28884  nmcexi  28885  nmcoplb  28889  lnfnmul  28907  nmbdfnlb  28909  nmcfnlb  28913  pjss2coi  29023  pjssmi  29024  isst  29072  ishst  29073  stcltr1i  29133  mdbr  29153  dmdbr  29158  mddmd2  29168  mdslmd1lem3  29186  mdslmd1lem4  29187  elat2  29199  atcvat2  29248  cdj1i  29292  vtocl2d  29314  rmoeqALT  29327  iuninc  29379  fmptcof2  29457  nnindd  29566  nn0min  29567  isomnd  29701  omndadd  29706  isarchi2  29739  archirng  29742  archiexdiv  29744  archiabl  29752  xrge0tsmsd  29785  isorng  29799  ofldchr  29814  crefeq  29912  nexple  30071  esumfzf  30131  issiga  30174  isrnsiga  30176  isldsys  30219  ismeas  30262  isrnmeas  30263  measiun  30281  eulerpartlemn  30443  sseqp1  30457  rrvsum  30516  signsply0  30628  signstfvc  30651  bnj941  30843  bnj106  30938  bnj155  30949  bnj590  30980  bnj591  30981  bnj849  30995  bnj893  30998  bnj944  31008  bnj1128  31058  subfacp1lem6  31167  erdszelem8  31180  issconn  31208  cvmliftlem7  31273  cvmliftlem10  31276  cvmlift3lem2  31302  mrsubvrs  31419  mclsssvlem  31459  mclsval  31460  mclsax  31466  mclsind  31467  shftvalg  31617  bccolsum  31625  iprodefisumlem  31626  faclimlem1  31629  dfpo2  31645  br1steqgOLD  31674  br2ndeqgOLD  31675  rdgprc  31700  trpredmintr  31731  frmin  31739  soseq  31751  frr3g  31779  nosupno  31849  nosupdm  31850  nosupfv  31852  nosupres  31853  nosupbnd1lem1  31854  nosupbnd1lem3  31856  nosupbnd1lem5  31858  noeta  31868  fveleq  32450  unblimceq0  32498  bj-axrep1  32788  bj-axrep2  32789  bj-axrep3  32790  rdgeqoa  33218  finxpreclem6  33233  wl-sblimt  33332  wl-sbhbt  33335  wl-2sb6d  33341  wl-mo2df  33352  wl-mo2t  33357  poimirlem2  33411  poimirlem25  33434  poimirlem28  33437  poimirlem31  33440  heicant  33444  mbfresfi  33456  itg2gt0cn  33465  sdclem2  33538  fdc  33541  seqpo  33543  incsequz  33544  mettrifi  33553  prdsbnd2  33594  heiborlem4  33613  bfplem1  33621  iscringd  33797  maxidlval  33838  igenval2  33865  iss2  34112  ax12eq  34226  ax12el  34227  ax12indalem  34230  ax12inda2ALT  34231  ax12inda  34233  ax12v2-o  34234  riotasvd  34242  isopos  34467  isat3  34594  ishlat1  34639  glbconN  34663  ispsubsp  35031  isldil  35396  isltrn  35405  isdilN  35441  trlval  35449  cdleme27b  35656  cdleme29b  35663  cdleme31sn1  35669  cdleme31sn1c  35676  cdleme40v  35757  cdlemk36  36201  cdlemkid5  36223  cdlemn11pre  36499  dihord2pre  36514  islpolN  36772  hdmapffval  37118  hdmapfval  37119  hdmapval2lem  37123  ismrc  37264  incssnn0  37274  mzpexpmpt  37308  pell14qrexpclnn0  37430  monotuz  37506  expmordi  37512  rmxypos  37514  jm2.17a  37527  jm2.17b  37528  rmygeid  37531  jm2.18  37555  jm2.19lem3  37558  jm2.25  37566  jm2.15nn0  37570  jm2.16nn0  37571  wepwsolem  37612  aomclem8  37631  dfac11  37632  pwslnm  37664  lnr2i  37686  hbtlem5  37698  cnsrexpcl  37735  rngunsnply  37743  isdomn3  37782  ifpbi23  37817  elmapintrab  37882  elmapintab  37902  cnvcnvintabd  37906  eliunov2  37971  relexpxpnnidm  37995  relexpiidm  37996  relexpss1d  37997  iunrelexpmin1  38000  relexpmulnn  38001  iunrelexpmin2  38004  relexp0a  38008  trclimalb2  38018  clsk3nimkb  38338  ntrclsiso  38365  ntrclskb  38367  ntrneiiso  38389  ntrneix2  38391  ntrneixb  38393  gneispace2  38430  gneispacess2  38444  dvgrat  38511  pm14.122b  38624  fnchoice  39188  fiiuncl  39234  ssinc  39264  ssdec  39265  wessf1ornlem  39371  dmrelrnrel  39419  fperiodmullem  39517  fmul01  39812  fmuldfeq  39815  climsuselem1  39839  climinff  39843  ellimcabssub0  39849  limcleqr  39876  addlimc  39880  0ellimcdiv  39881  limclner  39883  limsupref  39917  limsupub  39936  limsupmnf  39953  limsupre2lem  39956  limsupre2  39957  limsupre2mpt  39962  limsupre3lem  39964  limsupre3  39965  limsupre3mpt  39966  xlimbr  40053  cnrefiisplem  40055  dvnmptdivc  40153  dvnmptconst  40156  dvnmul  40158  iblspltprt  40189  itgspltprt  40195  stoweidlem2  40219  stoweidlem3  40220  stoweidlem17  40234  stoweidlem19  40236  stoweidlem21  40238  stoweidlem26  40243  fourierdlem42  40366  issal  40534  ismea  40668  isome  40708  carageniuncllem1  40735  caratheodorylem1  40740  2ffzoeq  41338  smonoord  41341  fargshiftf1  41377  perfectALTVlem2  41631  lmodvsmdi  42163  dmatALTval  42189  dmatALTbasel  42191  snlindsntor  42260  ldepsnlinc  42297  elbigo2r  42347  elbigolo1  42351  setrecseq  42432  setrec2fun  42439  setrec2lem2  42441