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  3490  3gencl  3491  vtocl2gf  3538  vtocl3gf  3539  vtocl2g  3540  vtocl3g  3541  vtocl2ga  3544  vtocl2gaf  3545  vtocl3gaf  3547  vtocl3ga  3549  vtocl4g  3551  vtocl4ga  3552  eqeu  3677  mo2icl  3685  euind  3695  reu7  3703  reuind  3724  sbctt  3823  sbccomlem  3832  reu8nf  3840  sbcnestgfw  4384  sbcnestgf  4389  r19.36zv  4470  dedth2h  4548  dedth3h  4549  dedth4h  4550  reusngf  4638  reuprg0  4666  preq12bg  4817  elint  4916  elintrabg  4925  intab  4942  axrep1  5235  axreplem  5236  axrep2  5237  axrep6g  5245  bm1.3iiOLD  5257  reusv3  5360  swopolem  5556  solin  5573  freq1  5605  frminex  5617  vtoclr  5701  2optocl  5734  3optocl  5735  raliunxp  5803  resieq  5961  iss  6006  cnveqb  6169  reu3op  6265  reuop  6266  dfpo2  6269  preddowncl  6305  funmoOLD  6532  funimaexgOLD  6604  fnbrfvb  6911  fvelimab  6933  fvmptss  6980  fmptco  7101  fprg  7127  fnressn  7130  fressnfv  7132  isoselem  7316  ovg  7554  caovcan  7593  caovordig  7594  caovord  7600  tfisi  7835  tfindsg  7837  tfinds2  7840  tfinds3  7841  dfom2  7844  elom  7845  findsg  7873  finds2  7874  resf1extb  7910  f1o2ndf1  8101  poxp  8107  fnse  8112  xpord3inddlem  8133  soseq  8138  fpr3g  8264  frrlem12  8276  fpr2a  8281  wfr3g  8298  smoeq  8319  smores  8321  smogt  8336  tfrlem1  8344  tfr3  8367  oaordi  8510  oeordi  8551  oeoa  8561  oeoe  8563  nnacl  8575  nnmcl  8576  nnecl  8577  nnacom  8581  nnaordi  8582  nnawordi  8585  nnaass  8586  nndi  8587  nnmass  8588  nnmsucr  8589  nnmcom  8590  nnmordi  8595  naddssim  8649  naddoa  8666  2ecoptocl  8781  3ecoptocl  8782  undifixp  8907  xpdom2g  9037  findcard2  9128  unfi  9135  ssfi  9137  fnfi  9142  fodomfi  9261  imafiOLD  9265  xpfiOLD  9270  fodomfiOLD  9281  finsschain  9310  marypha1lem  9384  marypha1  9385  supeq1  9396  ordiso2  9468  ordtypelem7  9477  wemaplem1  9499  inf3lem2  9582  inf3lem5  9585  infdiffi  9611  cantnfval2  9622  cantnfle  9624  cantnfp1lem3  9633  oemapval  9636  cantnflem1  9642  cantnf  9646  wemapwe  9650  cnfcom  9653  cnfcom3clem  9658  ttrclss  9673  ttrclselem2  9679  tz9.1  9682  frr3g  9709  frr2  9713  r1pwALT  9799  cplem2  9843  karden  9848  updjud  9887  infxpenc2lem2  9973  fseqenlem1  9977  dfac8clem  9985  alephinit  10048  dfac4  10075  dfac5lem5  10080  dfac2a  10083  dfac2b  10084  dfacacn  10095  dfac12lem3  10099  kmlem2  10105  kmlem13  10116  nnadju  10151  ackbij1lem16  10187  sornom  10230  infpssrlem4  10259  fin23lem14  10286  fin23lem32  10297  fin23lem34  10299  fin23lem36  10301  isf32lem1  10306  isf32lem2  10307  axcc2lem  10389  axcc3  10391  axcclem  10410  zornn0g  10458  ttukeylem5  10466  ttukeylem6  10467  axrepnd  10547  axpowndlem3  10552  zfcndrep  10567  fpwwe2lem7  10590  pwfseqlem3  10613  wunr1om  10672  wunfi  10674  tskr1om  10720  ingru  10768  grudomon  10770  axgroth3  10784  axgroth4  10785  nqereu  10882  mulcanenq  10913  elnp  10940  elnpi  10941  prlem934  10986  infm3  12142  nnindd  12206  nnaddcl  12209  nnmulcl  12210  nnne0  12220  peano5uzi  12623  uzind2  12627  nn0indd  12631  zindd  12635  fzindd  12636  eluzaddOLD  12828  uzaddcl  12863  uzwo  12870  indstr  12875  zmax  12904  xmulasslem  13245  xrsupsslem  13267  xrinfmsslem  13268  xrsupss  13269  xrinfmss  13270  flval2  13776  om2uzlti  13915  uzrdgfni  13923  rabssnn0fi  13951  mptnn0fsupp  13962  seqcl2  13985  seqfveq2  13989  seqshft2  13993  monoord  13997  seqsplit  14000  seqcaopr3  14002  seqf1olem2a  14005  seqf1o  14008  seqid2  14013  seqhomo  14014  ser1const  14023  expcllem  14037  expeq0  14057  mulexp  14066  expadd  14069  expmul  14072  expmordi  14132  leexp2r  14139  leexp1a  14140  bernneq  14194  modexp  14203  facdiv  14252  faclbnd  14255  faclbnd4lem4  14261  hashgadd  14342  hashxp  14399  hashmap  14400  hashf1lem2  14421  hashf1  14422  seqcoll  14429  wrdind  14687  wrd2ind  14688  pfxccatin12lem3  14697  cshweqrep  14786  2cshwcshw  14791  relexp0g  14988  relexpsucnnr  14991  relexpsucnnl  14996  relexpcnv  15001  relexpnndm  15007  relexpaddnn  15017  rtrclreclem1  15023  dfrtrclrec2  15024  rtrclreclem2  15025  rtrclreclem4  15027  dfrtrcl2  15028  relexpind  15030  reusq0  15431  rlim  15461  rlim2  15462  rlim0  15474  rlim0lt  15475  rlimi  15479  ello12r  15483  ello1mpt  15487  ello1d  15489  elo12r  15494  lo1o1  15498  o1lo1  15503  lo1res  15525  climshft  15542  o1compt  15553  rlimo1  15583  lo1add  15593  lo1mul  15594  rlimdiv  15612  climub  15628  climserle  15629  caucvgrlem  15639  caurcvgr  15640  iseraltlem2  15649  summolem2a  15681  sumss  15690  fsum2d  15737  fsumabs  15767  fsumrlim  15777  fsumo1  15778  fsumiun  15787  binom  15796  climcndslem1  15815  climcndslem2  15816  cvgrat  15849  clim2prod  15854  prodfn0  15860  prodfrec  15861  ntrivcvgfvn0  15865  prodmolem2a  15900  fprodabs  15940  fprodn0  15945  fprod2d  15947  binomfallfac  16007  bpolycl  16018  bpolydif  16021  fprodefsum  16061  demoivreALT  16169  ruclem8  16205  ruclem9  16206  dvdsle  16280  dvdsfac  16296  divalglem7  16369  bitsinv1  16412  sadcadd  16428  sadadd2  16430  saddisjlem  16434  smuval2  16452  smupvallem  16453  smu01lem  16455  smupval  16458  smueqlem  16460  smumullem  16462  bezoutlem4  16512  dfgcd2  16516  rplpwr  16528  nn0seqcvgd  16540  seq1st  16541  alginv  16545  algcvga  16549  algfx  16550  lcmf  16603  prmind2  16655  prmdvdsexp  16685  prmfac1  16690  reumodprminv  16775  pcmpt  16863  pcfac  16870  prmpwdvds  16875  prmreclem4  16890  vdwlem10  16961  ramval  16979  ramcl  17000  cshwrepswhash1  17073  prmlem1a  17077  imasleval  17504  ismre  17551  mreexexd  17609  lubprop  18317  lublecllem  18319  glbprop  18330  joinlem  18342  meetlem  18356  poslubmo  18370  posglbmo  18371  poslubd  18372  isglbd  18468  lubun  18474  mndind  18755  frmdgsum  18789  mulgnnass  19041  mhmmulg  19047  gsumwrev  19298  gsmsymgrfix  19358  gsmsymgreq  19362  psgnunilem3  19426  sylow1lem1  19528  efginvrel2  19657  efgsrel  19664  efgredlemd  19674  efgredlem  19677  efgred  19678  efgrelexlemb  19680  gsum2dlem2  19901  gsumcom2  19905  ablfac1eulem  20004  pgpfac1lem2  20007  pgpfac1lem5  20011  pgpfac1  20012  pgpfac  20016  srgmulgass  20126  srgpcomp  20127  srgbinom  20140  isdomn2OLD  20621  isdomn3  20624  lmodvsmmulgdi  20803  cnfldexp  21316  islindf4  21747  assamulgscm  21810  mplcoe1  21944  mplcoe3  21945  mplcoe5  21947  gsummoncoe1  22195  dmatval  22379  dmatel  22380  dmatmulcl  22387  pmatcoe1fsupp  22588  decpmataa0  22655  decpmatmulsumfsupp  22660  pmatcollpw2lem  22664  pm2mpmhmlem1  22705  fiinopn  22788  mretopd  22979  neiptoptop  23018  cnpfval  23121  iscnp3  23131  tgcn  23139  lmbr  23145  lmbr2  23146  lmbrf  23147  lmss  23185  ishaus  23209  hausnei2  23240  t1sep2  23256  fiuncmp  23291  dfconn2  23306  1stcfb  23332  2ndc1stc  23338  1stcrest  23340  1stcelcls  23348  1stccn  23350  lly1stc  23383  elkgen  23423  kgencn  23443  tx1stc  23537  xkopt  23542  cnmptcom  23565  isr0  23624  r0sep  23635  ptcmpfi  23700  isfildlem  23744  rnelfm  23840  fbflim  23863  flimrest  23870  isflf  23880  flffbas  23882  lmflf  23892  fclsrest  23911  isfcf  23921  cnextfvval  23952  tmdgsum  23982  eltsms  24020  tsmsi  24021  tsmsgsum  24026  tsmssubm  24030  tsmsres  24031  tsmsf1o  24032  isust  24091  isucn  24165  isucn2  24166  ucnima  24168  imasdsf1olem  24261  metss  24396  met1stc  24409  metcnp  24429  metcnpi  24432  metcnpi2  24433  metucn  24459  xrge0tsms  24723  fsumcn  24761  elcncf  24782  cncfi  24787  rescncf  24790  cncfco  24800  caucfil  25183  equivcau  25200  caubl  25208  caublcls  25209  ovolgelb  25381  ovolunlem1a  25397  ovolicc2lem3  25420  voliunlem1  25451  voliunlem3  25453  volsuplem  25456  volsup  25457  dyadmax  25499  vitali  25514  itg2leub  25635  itgfsum  25728  dvnadd  25831  dvnres  25833  cpnord  25837  dvnfre  25856  dvmptfsum  25879  dvferm1  25889  dvferm2  25891  rolle  25894  dvlip  25898  c1lip1  25902  lhop1  25919  deg1leb  26000  ply1divex  26042  fta1g  26075  plyco  26146  dgrcolem1  26179  dgrco  26181  dvnply2  26195  plydivex  26205  aalioulem2  26241  aalioulem3  26242  aalioulem5  26244  aaliou3lem2  26251  dvntaylp  26279  taylthlem1  26281  ulmdvlem3  26311  abelthlem9  26350  cxpmul2  26598  scvxcvx  26896  jensenlem2  26898  jensen  26899  wilthlem3  26980  perfectlem2  27141  bcmono  27188  bposlem5  27199  lgsquad2lem2  27296  addsq2reu  27351  2sqreulem1  27357  2sqreunnlem1  27360  dchrisumlem1  27400  dchrisum0flb  27421  pntpbnd1  27497  pntlemf  27516  qabvle  27536  qabvexp  27537  ostthlem2  27539  ostth2lem2  27545  nosupcbv  27614  nosupno  27615  nosupdm  27616  nosupfv  27618  nosupres  27619  nosupbnd1lem1  27620  nosupbnd1lem3  27622  nosupbnd1lem5  27624  noinfcbv  27629  noinfno  27630  noinfdm  27631  noinffv  27633  noinfres  27634  noinfbnd1lem3  27637  noinfbnd1lem5  27639  eqscut2  27718  addsproplem1  27876  addsprop  27883  negsunif  27961  mulsproplem9  28027  ssltmul2  28051  precsexlem8  28116  precsexlem9  28117  precsexlem11  28119  noseqind  28186  om2noseqrdg  28198  noseqrdgfn  28200  n0addscl  28236  n0mulscl  28237  eucliddivs  28265  peano5uzs  28292  expscllem  28316  expadds  28320  expsne0  28321  expsgt0  28322  pw2cut  28335  tgcgr4  28458  usgr2pth  29694  wlkiswwlks2lem4  29802  wlkiswwlks2  29805  rusgrnumwwlk  29905  clwlkclwwlklem2a  29927  clwlkclwwlklem1  29928  clwlkclwwlkfo  29938  eupth2  30168  frgr3vlem1  30202  3vfriswmgrlem  30206  3vfriswmgr  30207  wlkl0  30296  numclwlk2lem2f1o  30308  isplig  30405  isnvlem  30539  nvi  30543  nmoubi  30701  nmounbi  30705  nmblolbi  30729  ipasslem1  30760  ipassi  30770  hlim2  31121  pjhth  31322  spansni  31486  elspansn2  31496  pjige0  31620  pjcjt2  31621  pjopyth  31649  elcnop  31786  elcnfn  31811  nmopub  31837  cnopc  31842  nmfnleub  31854  elnlfn  31857  cnfnc  31859  nmbdoplb  31954  nmcexi  31955  nmcoplb  31959  lnfnmul  31977  nmbdfnlb  31979  nmcfnlb  31983  pjss2coi  32093  pjssmi  32094  isst  32142  ishst  32143  stcltr1i  32203  mdbr  32223  dmdbr  32228  mddmd2  32238  mdslmd1lem3  32256  mdslmd1lem4  32257  elat2  32269  atcvat2  32318  cdj1i  32362  iuninc  32489  fmptcof2  32581  nn0min  32745  nexple  32769  wrdt2ind  32875  ismnt  32909  xrge0tsmsd  33002  gsumwun  33005  isomnd  33015  omndadd  33020  cyc3genpm  33109  isarchi2  33139  archirng  33142  archiexdiv  33144  archiabl  33152  domnprodn0  33226  isorng  33277  ofldchr  33292  islbs5  33351  unitprodclb  33360  mxidlval  33432  1arithidom  33508  1arithufdlem3  33517  crefeq  33835  esumfzf  34059  issiga  34102  isrnsiga  34103  isldsys  34146  ismeas  34189  isrnmeas  34190  measiun  34208  eulerpartlemn  34372  sseqp1  34386  rrvsum  34445  signsply0  34542  signstfvc  34565  bnj941  34762  bnj106  34858  bnj155  34869  bnj590  34900  bnj591  34901  bnj849  34915  bnj893  34918  bnj944  34928  bnj1128  34980  gblacfnacd  35089  subfacp1lem6  35172  erdszelem8  35185  issconn  35213  cvmliftlem7  35278  cvmliftlem10  35281  cvmlift3lem2  35307  satfsschain  35351  satfrel  35354  satfdm  35356  satfrnmapom  35357  fmlafvel  35372  satffun  35396  mrsubvrs  35509  mclsssvlem  35549  mclsval  35550  mclsax  35556  mclsind  35557  shftvalg  35719  bccolsum  35726  iprodefisumlem  35727  faclimlem1  35730  rdgprc  35782  sbequbidv  36202  cbvsbdavw  36242  fveleq  36439  unblimceq0  36495  bj-ax12  36645  bj-bm1.3ii  37052  rdgeqoa  37358  finxpreclem6  37384  domalom  37392  ralssiun  37395  wl-ax12v2cl  37494  wl-sblimt  37536  wl-sbhbt  37542  wl-2sb6d  37546  wl-mo2df  37558  wl-mo2t  37563  poimirlem2  37616  poimirlem25  37639  poimirlem28  37642  poimirlem31  37645  heicant  37649  mbfresfi  37660  itg2gt0cn  37669  sdclem2  37736  fdc  37739  seqpo  37741  incsequz  37742  mettrifi  37751  prdsbnd2  37789  heiborlem4  37808  bfplem1  37816  iscringd  37992  maxidlval  38033  igenval2  38060  iss2  38326  elrefrels3  38510  ax12eq  38934  ax12el  38935  ax12indalem  38938  ax12inda2ALT  38939  ax12inda  38941  ax12v2-o  38942  riotasvd  38949  isopos  39173  isat3  39300  ishlat1  39345  glbconN  39370  glbconNOLD  39371  ispsubsp  39739  isldil  40104  isltrn  40113  isdilN  40148  trlval  40156  cdleme27b  40362  cdleme29b  40369  cdleme31sn1  40375  cdleme31sn1c  40382  cdleme40v  40463  cdlemk36  40907  cdlemkid5  40929  cdlemn11pre  41204  dihord2pre  41219  islpolN  41477  hdmapffval  41820  hdmapfval  41821  hdmapval2lem  41825  uzindd  41965  sticksstones1  42134  sticksstones2  42135  sticksstones3  42136  sticksstones8  42141  sticksstones10  42143  sticksstones11  42144  sticksstones12a  42145  sticksstones15  42149  indstrd  42181  unitscyglem3  42185  nnaddcom  42256  nnadddir  42258  nnmulcom  42260  eu6w  42664  ismrc  42689  incssnn0  42699  mzpexpmpt  42733  pell14qrexpclnn0  42854  monotuz  42930  rmxypos  42936  jm2.17a  42949  jm2.17b  42950  rmygeid  42953  jm2.18  42977  jm2.19lem3  42980  jm2.25  42988  jm2.15nn0  42992  jm2.16nn0  42993  wepwsolem  43031  aomclem8  43050  dfac11  43051  pwslnm  43083  lnr2i  43105  hbtlem5  43117  cnsrexpcl  43154  rngunsnply  43158  unielss  43207  onsucf1lem  43258  cantnfresb  43313  onmcl  43320  naddonnn  43384  elmapintrab  43565  elmapintab  43585  cnvcnvintabd  43589  eliunov2  43668  relexpxpnnidm  43692  relexpiidm  43693  relexpss1d  43694  iunrelexpmin1  43697  relexpmulnn  43698  iunrelexpmin2  43701  relexp0a  43705  trclimalb2  43715  clsk3nimkb  44029  ntrclsiso  44056  ntrclskb  44058  ntrneiiso  44080  ntrneix2  44082  ntrneixb  44084  gneispace2  44121  gneispacess2  44135  mnuunid  44266  dvgrat  44301  pm14.122b  44412  relpeq1  44934  relpeq3  44936  trfr  44952  pwclaxpow  44974  prclaxpr  44975  uniclaxun  44976  modelac8prim  44982  permaxpow  44999  permaxpr  45000  permaxun  45001  nregmodel  45007  fnchoice  45023  fiiuncl  45059  ssinc  45081  ssdec  45082  wessf1ornlem  45179  dmrelrnrel  45220  fperiodmullem  45301  monoordxrv  45477  fmul01  45578  fmuldfeq  45581  climsuselem1  45605  climinff  45609  ellimcabssub0  45615  limcleqr  45642  addlimc  45646  0ellimcdiv  45647  limclner  45649  limsupref  45683  limsupub  45702  limsupmnf  45719  limsupre2lem  45722  limsupre2  45723  limsupre2mpt  45728  limsupre3lem  45730  limsupre3  45731  limsupre3mpt  45732  xlimbr  45825  cnrefiisplem  45827  dvnmptdivc  45936  dvnmptconst  45939  dvnmul  45941  iblspltprt  45971  itgspltprt  45977  stoweidlem2  46000  stoweidlem3  46001  stoweidlem17  46015  stoweidlem19  46017  stoweidlem21  46019  stoweidlem26  46024  fourierdlem42  46147  issal  46312  ismea  46449  isome  46492  carageniuncllem1  46519  caratheodorylem1  46524  2reu8i  47114  2reuimp0  47115  funressndmafv2rn  47224  2ffzoeq  47328  smonoord  47372  fargshiftf1  47442  ichnfimlem  47464  paireqne  47512  reupr  47523  reuopreuprim  47527  perfectALTVlem2  47723  grimcnv  47888  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem4  48109  pgnbgreunbgr  48115  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