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  2209  axc14  2466  mojust  2537  mof  2561  eu6lem  2571  2gencl  3508  3gencl  3509  vtocl2gf  3556  vtocl3gf  3557  vtocl2g  3558  vtocl3g  3559  vtocl2ga  3562  vtocl2gaf  3563  vtocl3gaf  3565  vtocl3ga  3567  vtocl4g  3569  vtocl4ga  3570  eqeu  3696  mo2icl  3704  euind  3714  reu7  3722  reuind  3743  sbctt  3842  sbccomlem  3851  reu8nf  3859  sbcnestgfw  4403  sbcnestgf  4408  r19.36zv  4489  dedth2h  4567  dedth3h  4568  dedth4h  4569  reusngf  4656  reuprg0  4684  preq12bg  4835  elint  4934  elintrabg  4943  intab  4960  axrep1  5262  axreplem  5263  axrep2  5264  axrep6g  5272  bm1.3iiOLD  5284  reusv3  5387  swopolem  5584  solin  5601  freq1  5634  frminex  5646  vtoclr  5730  2optocl  5763  3optocl  5764  raliunxp  5832  resieq  5990  iss  6035  cnveqb  6198  reu3op  6294  reuop  6295  dfpo2  6298  preddowncl  6334  funmoOLD  6563  funimaexgOLD  6635  fnbrfvb  6940  fvelimab  6962  fvmptss  7009  fmptco  7130  fprg  7156  fnressn  7159  fressnfv  7161  isoselem  7344  ovg  7581  caovcan  7620  caovordig  7621  caovord  7627  tfisi  7863  tfindsg  7865  tfinds2  7868  tfinds3  7869  dfom2  7872  elom  7873  findsg  7902  finds2  7903  resf1extb  7939  f1o2ndf1  8130  poxp  8136  fnse  8141  xpord3inddlem  8162  soseq  8167  fpr3g  8293  frrlem12  8305  fpr2a  8310  wfr3g  8330  wfrlem4OLD  8335  smoeq  8373  smores  8375  smogt  8390  tfrlem1  8399  tfr3  8422  oaordi  8567  oeordi  8608  oeoa  8618  oeoe  8620  nnacl  8632  nnmcl  8633  nnecl  8634  nnacom  8638  nnaordi  8639  nnawordi  8642  nnaass  8643  nndi  8644  nnmass  8645  nnmsucr  8646  nnmcom  8647  nnmordi  8652  naddssim  8706  naddoa  8723  2ecoptocl  8831  3ecoptocl  8832  undifixp  8957  xpdom2g  9091  findcard2  9187  unfi  9194  ssfi  9196  fnfi  9201  fodomfi  9333  imafiOLD  9337  xpfiOLD  9342  fodomfiOLD  9353  finsschain  9382  marypha1lem  9456  marypha1  9457  supeq1  9468  ordiso2  9538  ordtypelem7  9547  wemaplem1  9569  inf3lem2  9652  inf3lem5  9655  infdiffi  9681  cantnfval2  9692  cantnfle  9694  cantnfp1lem3  9703  oemapval  9706  cantnflem1  9712  cantnf  9716  wemapwe  9720  cnfcom  9723  cnfcom3clem  9728  ttrclss  9743  ttrclselem2  9749  tz9.1  9752  frr3g  9779  frr2  9783  r1pwALT  9869  cplem2  9913  karden  9918  updjud  9957  infxpenc2lem2  10043  fseqenlem1  10047  dfac8clem  10055  alephinit  10118  dfac4  10145  dfac5lem5  10150  dfac2a  10153  dfac2b  10154  dfacacn  10165  dfac12lem3  10169  kmlem2  10175  kmlem13  10186  nnadju  10221  ackbij1lem16  10257  sornom  10300  infpssrlem4  10329  fin23lem14  10356  fin23lem32  10367  fin23lem34  10369  fin23lem36  10371  isf32lem1  10376  isf32lem2  10377  axcc2lem  10459  axcc3  10461  axcclem  10480  zornn0g  10528  ttukeylem5  10536  ttukeylem6  10537  axrepnd  10617  axpowndlem3  10622  zfcndrep  10637  fpwwe2lem7  10660  pwfseqlem3  10683  wunr1om  10742  wunfi  10744  tskr1om  10790  ingru  10838  grudomon  10840  axgroth3  10854  axgroth4  10855  nqereu  10952  mulcanenq  10983  elnp  11010  elnpi  11011  prlem934  11056  infm3  12210  nnindd  12269  nnaddcl  12272  nnmulcl  12273  nnne0  12283  peano5uzi  12691  uzind2  12695  nn0indd  12699  zindd  12703  fzindd  12704  eluzaddOLD  12896  uzaddcl  12929  uzwo  12936  indstr  12941  zmax  12970  xmulasslem  13310  xrsupsslem  13332  xrinfmsslem  13333  xrsupss  13334  xrinfmss  13335  flval2  13837  om2uzlti  13974  uzrdgfni  13982  rabssnn0fi  14010  mptnn0fsupp  14021  seqcl2  14044  seqfveq2  14048  seqshft2  14052  monoord  14056  seqsplit  14059  seqcaopr3  14061  seqf1olem2a  14064  seqf1o  14067  seqid2  14072  seqhomo  14073  ser1const  14082  expcllem  14096  expeq0  14116  mulexp  14125  expadd  14128  expmul  14131  expmordi  14190  leexp2r  14197  leexp1a  14198  bernneq  14251  modexp  14260  facdiv  14309  faclbnd  14312  faclbnd4lem4  14318  hashgadd  14399  hashxp  14456  hashmap  14457  hashf1lem2  14478  hashf1  14479  seqcoll  14486  wrdind  14743  wrd2ind  14744  pfxccatin12lem3  14753  cshweqrep  14842  2cshwcshw  14847  relexp0g  15044  relexpsucnnr  15047  relexpsucnnl  15052  relexpcnv  15057  relexpnndm  15063  relexpaddnn  15073  rtrclreclem1  15079  dfrtrclrec2  15080  rtrclreclem2  15081  rtrclreclem4  15083  dfrtrcl2  15084  relexpind  15086  reusq0  15484  rlim  15514  rlim2  15515  rlim0  15527  rlim0lt  15528  rlimi  15532  ello12r  15536  ello1mpt  15540  ello1d  15542  elo12r  15547  lo1o1  15551  o1lo1  15556  lo1res  15578  climshft  15595  o1compt  15606  rlimo1  15636  lo1add  15646  lo1mul  15647  rlimdiv  15665  climub  15681  climserle  15682  caucvgrlem  15692  caurcvgr  15693  iseraltlem2  15702  summolem2a  15734  sumss  15743  fsum2d  15790  fsumabs  15820  fsumrlim  15830  fsumo1  15831  fsumiun  15840  binom  15849  climcndslem1  15868  climcndslem2  15869  cvgrat  15902  clim2prod  15907  prodfn0  15913  prodfrec  15914  ntrivcvgfvn0  15918  prodmolem2a  15953  fprodabs  15993  fprodn0  15998  fprod2d  16000  binomfallfac  16060  bpolycl  16071  bpolydif  16074  fprodefsum  16114  demoivreALT  16220  ruclem8  16256  ruclem9  16257  dvdsle  16330  dvdsfac  16346  divalglem7  16419  bitsinv1  16462  sadcadd  16478  sadadd2  16480  saddisjlem  16484  smuval2  16502  smupvallem  16503  smu01lem  16505  smupval  16508  smueqlem  16510  smumullem  16512  bezoutlem4  16562  dfgcd2  16566  rplpwr  16578  nn0seqcvgd  16590  seq1st  16591  alginv  16595  algcvga  16599  algfx  16600  lcmf  16653  prmind2  16705  prmdvdsexp  16735  prmfac1  16740  reumodprminv  16825  pcmpt  16913  pcfac  16920  prmpwdvds  16925  prmreclem4  16940  vdwlem10  17011  ramval  17029  ramcl  17050  cshwrepswhash1  17123  prmlem1a  17127  imasleval  17562  ismre  17609  mreexexd  17667  lubprop  18377  lublecllem  18379  glbprop  18390  joinlem  18402  meetlem  18416  poslubmo  18430  posglbmo  18431  poslubd  18432  isglbd  18528  lubun  18534  mndind  18815  frmdgsum  18849  mulgnnass  19101  mhmmulg  19107  gsumwrev  19358  gsmsymgrfix  19419  gsmsymgreq  19423  psgnunilem3  19487  sylow1lem1  19589  efginvrel2  19718  efgsrel  19725  efgredlemd  19735  efgredlem  19738  efgred  19739  efgrelexlemb  19741  gsum2dlem2  19962  gsumcom2  19966  ablfac1eulem  20065  pgpfac1lem2  20068  pgpfac1lem5  20072  pgpfac1  20073  pgpfac  20077  srgmulgass  20187  srgpcomp  20188  srgbinom  20201  isdomn2OLD  20685  isdomn3  20688  lmodvsmmulgdi  20868  cnfldexp  21384  islindf4  21825  assamulgscm  21888  mplcoe1  22022  mplcoe3  22023  mplcoe5  22025  gsummoncoe1  22279  dmatval  22465  dmatel  22466  dmatmulcl  22473  pmatcoe1fsupp  22674  decpmataa0  22741  decpmatmulsumfsupp  22746  pmatcollpw2lem  22750  pm2mpmhmlem1  22791  fiinopn  22874  mretopd  23065  neiptoptop  23104  cnpfval  23207  iscnp3  23217  tgcn  23225  lmbr  23231  lmbr2  23232  lmbrf  23233  lmss  23271  ishaus  23295  hausnei2  23326  t1sep2  23342  fiuncmp  23377  dfconn2  23392  1stcfb  23418  2ndc1stc  23424  1stcrest  23426  1stcelcls  23434  1stccn  23436  lly1stc  23469  elkgen  23509  kgencn  23529  tx1stc  23623  xkopt  23628  cnmptcom  23651  isr0  23710  r0sep  23721  ptcmpfi  23786  isfildlem  23830  rnelfm  23926  fbflim  23949  flimrest  23956  isflf  23966  flffbas  23968  lmflf  23978  fclsrest  23997  isfcf  24007  cnextfvval  24038  tmdgsum  24068  eltsms  24106  tsmsi  24107  tsmsgsum  24112  tsmssubm  24116  tsmsres  24117  tsmsf1o  24118  isust  24177  isucn  24251  isucn2  24252  ucnima  24254  imasdsf1olem  24347  metss  24484  met1stc  24497  metcnp  24517  metcnpi  24520  metcnpi2  24521  metucn  24547  xrge0tsms  24811  fsumcn  24849  elcncf  24870  cncfi  24875  rescncf  24878  cncfco  24888  caucfil  25272  equivcau  25289  caubl  25297  caublcls  25298  ovolgelb  25470  ovolunlem1a  25486  ovolicc2lem3  25509  voliunlem1  25540  voliunlem3  25542  volsuplem  25545  volsup  25546  dyadmax  25588  vitali  25603  itg2leub  25724  itgfsum  25817  dvnadd  25920  dvnres  25922  cpnord  25926  dvnfre  25945  dvmptfsum  25968  dvferm1  25978  dvferm2  25980  rolle  25983  dvlip  25987  c1lip1  25991  lhop1  26008  deg1leb  26089  ply1divex  26131  fta1g  26164  plyco  26235  dgrcolem1  26268  dgrco  26270  dvnply2  26284  plydivex  26294  aalioulem2  26330  aalioulem3  26331  aalioulem5  26333  aaliou3lem2  26340  dvntaylp  26368  taylthlem1  26370  ulmdvlem3  26400  abelthlem9  26439  cxpmul2  26686  scvxcvx  26984  jensenlem2  26986  jensen  26987  wilthlem3  27068  perfectlem2  27229  bcmono  27276  bposlem5  27287  lgsquad2lem2  27384  addsq2reu  27439  2sqreulem1  27445  2sqreunnlem1  27448  dchrisumlem1  27488  dchrisum0flb  27509  pntpbnd1  27585  pntlemf  27604  qabvle  27624  qabvexp  27625  ostthlem2  27627  ostth2lem2  27633  nosupcbv  27702  nosupno  27703  nosupdm  27704  nosupfv  27706  nosupres  27707  nosupbnd1lem1  27708  nosupbnd1lem3  27710  nosupbnd1lem5  27712  noinfcbv  27717  noinfno  27718  noinfdm  27719  noinffv  27721  noinfres  27722  noinfbnd1lem3  27725  noinfbnd1lem5  27727  eqscut2  27806  addsproplem1  27957  addsprop  27964  negsunif  28042  mulsproplem9  28105  ssltmul2  28129  precsexlem8  28193  precsexlem9  28194  precsexlem11  28196  noseqind  28253  om2noseqrdg  28265  noseqrdgfn  28267  n0addscl  28302  n0mulscl  28303  peano5uzs  28345  expscl  28368  expsne0  28369  expsgt0  28370  pw2cut  28375  tgcgr4  28494  usgr2pth  29731  wlkiswwlks2lem4  29839  wlkiswwlks2  29842  rusgrnumwwlk  29942  clwlkclwwlklem2a  29964  clwlkclwwlklem1  29965  clwlkclwwlkfo  29975  eupth2  30205  frgr3vlem1  30239  3vfriswmgrlem  30243  3vfriswmgr  30244  wlkl0  30333  numclwlk2lem2f1o  30345  isplig  30442  isnvlem  30576  nvi  30580  nmoubi  30738  nmounbi  30742  nmblolbi  30766  ipasslem1  30797  ipassi  30807  hlim2  31158  pjhth  31359  spansni  31523  elspansn2  31533  pjige0  31657  pjcjt2  31658  pjopyth  31686  elcnop  31823  elcnfn  31848  nmopub  31874  cnopc  31879  nmfnleub  31891  elnlfn  31894  cnfnc  31896  nmbdoplb  31991  nmcexi  31992  nmcoplb  31996  lnfnmul  32014  nmbdfnlb  32016  nmcfnlb  32020  pjss2coi  32130  pjssmi  32131  isst  32179  ishst  32180  stcltr1i  32240  mdbr  32260  dmdbr  32265  mddmd2  32275  mdslmd1lem3  32293  mdslmd1lem4  32294  elat2  32306  atcvat2  32355  cdj1i  32399  iuninc  32520  fmptcof2  32614  nn0min  32769  nexple  32780  wrdt2ind  32885  ismnt  32919  xrge0tsmsd  33011  gsumwun  33014  isomnd  33024  omndadd  33029  cyc3genpm  33118  isarchi2  33138  archirng  33141  archiexdiv  33143  archiabl  33151  domnprodn0  33225  isorng  33275  ofldchr  33290  islbs5  33349  unitprodclb  33358  mxidlval  33430  1arithidom  33506  1arithufdlem3  33515  crefeq  33785  esumfzf  34011  issiga  34054  isrnsiga  34055  isldsys  34098  ismeas  34141  isrnmeas  34142  measiun  34160  eulerpartlemn  34324  sseqp1  34338  rrvsum  34397  signsply0  34507  signstfvc  34530  bnj941  34727  bnj106  34823  bnj155  34834  bnj590  34865  bnj591  34866  bnj849  34880  bnj893  34883  bnj944  34893  bnj1128  34945  gblacfnacd  35054  subfacp1lem6  35131  erdszelem8  35144  issconn  35172  cvmliftlem7  35237  cvmliftlem10  35240  cvmlift3lem2  35266  satfsschain  35310  satfrel  35313  satfdm  35315  satfrnmapom  35316  fmlafvel  35331  satffun  35355  mrsubvrs  35468  mclsssvlem  35508  mclsval  35509  mclsax  35515  mclsind  35516  shftvalg  35673  bccolsum  35680  iprodefisumlem  35681  faclimlem1  35684  rdgprc  35736  sbequbidv  36156  cbvsbdavw  36196  fveleq  36393  unblimceq0  36449  bj-ax12  36599  bj-bm1.3ii  37006  rdgeqoa  37312  finxpreclem6  37338  domalom  37346  ralssiun  37349  wl-ax12v2cl  37448  wl-sblimt  37490  wl-sbhbt  37496  wl-2sb6d  37500  wl-mo2df  37512  wl-mo2t  37517  poimirlem2  37570  poimirlem25  37593  poimirlem28  37596  poimirlem31  37599  heicant  37603  mbfresfi  37614  itg2gt0cn  37623  sdclem2  37690  fdc  37693  seqpo  37695  incsequz  37696  mettrifi  37705  prdsbnd2  37743  heiborlem4  37762  bfplem1  37770  iscringd  37946  maxidlval  37987  igenval2  38014  iss2  38286  elrefrels3  38461  ax12eq  38883  ax12el  38884  ax12indalem  38887  ax12inda2ALT  38888  ax12inda  38890  ax12v2-o  38891  riotasvd  38898  isopos  39122  isat3  39249  ishlat1  39294  glbconN  39319  glbconNOLD  39320  ispsubsp  39688  isldil  40053  isltrn  40062  isdilN  40097  trlval  40105  cdleme27b  40311  cdleme29b  40318  cdleme31sn1  40324  cdleme31sn1c  40331  cdleme40v  40412  cdlemk36  40856  cdlemkid5  40878  cdlemn11pre  41153  dihord2pre  41168  islpolN  41426  hdmapffval  41769  hdmapfval  41770  hdmapval2lem  41774  uzindd  41919  sticksstones1  42088  sticksstones2  42089  sticksstones3  42090  sticksstones8  42095  sticksstones10  42097  sticksstones11  42098  sticksstones12a  42099  sticksstones15  42103  indstrd  42135  unitscyglem3  42139  nnaddcom  42248  nnadddir  42250  nnmulcom  42252  eu6w  42631  ismrc  42657  incssnn0  42667  mzpexpmpt  42701  pell14qrexpclnn0  42822  monotuz  42898  rmxypos  42904  jm2.17a  42917  jm2.17b  42918  rmygeid  42921  jm2.18  42945  jm2.19lem3  42948  jm2.25  42956  jm2.15nn0  42960  jm2.16nn0  42961  wepwsolem  42999  aomclem8  43018  dfac11  43019  pwslnm  43051  lnr2i  43073  hbtlem5  43085  cnsrexpcl  43122  rngunsnply  43126  unielss  43175  onsucf1lem  43227  cantnfresb  43282  onmcl  43289  naddonnn  43353  elmapintrab  43534  elmapintab  43554  cnvcnvintabd  43558  eliunov2  43637  relexpxpnnidm  43661  relexpiidm  43662  relexpss1d  43663  iunrelexpmin1  43666  relexpmulnn  43667  iunrelexpmin2  43670  relexp0a  43674  trclimalb2  43684  clsk3nimkb  43998  ntrclsiso  44025  ntrclskb  44027  ntrneiiso  44049  ntrneix2  44051  ntrneixb  44053  gneispace2  44090  gneispacess2  44104  mnuunid  44241  dvgrat  44276  pm14.122b  44387  relpeq1  44910  relpeq3  44912  trfr  44924  pwclaxpow  44946  prclaxpr  44947  uniclaxun  44948  modelac8prim  44954  fnchoice  44979  fiiuncl  45015  ssinc  45037  ssdec  45038  wessf1ornlem  45135  dmrelrnrel  45176  fperiodmullem  45260  monoordxrv  45437  fmul01  45540  fmuldfeq  45543  climsuselem1  45567  climinff  45571  ellimcabssub0  45577  limcleqr  45604  addlimc  45608  0ellimcdiv  45609  limclner  45611  limsupref  45645  limsupub  45664  limsupmnf  45681  limsupre2lem  45684  limsupre2  45685  limsupre2mpt  45690  limsupre3lem  45692  limsupre3  45693  limsupre3mpt  45694  xlimbr  45787  cnrefiisplem  45789  dvnmptdivc  45898  dvnmptconst  45901  dvnmul  45903  iblspltprt  45933  itgspltprt  45939  stoweidlem2  45962  stoweidlem3  45963  stoweidlem17  45977  stoweidlem19  45979  stoweidlem21  45981  stoweidlem26  45986  fourierdlem42  46109  issal  46274  ismea  46411  isome  46454  carageniuncllem1  46481  caratheodorylem1  46486  2reu8i  47071  2reuimp0  47072  funressndmafv2rn  47181  2ffzoeq  47285  smonoord  47304  fargshiftf1  47374  ichnfimlem  47396  paireqne  47444  reupr  47455  reuopreuprim  47459  perfectALTVlem2  47655  grimcnv  47825  lmodvsmdi  48241  dmatALTval  48263  dmatALTbasel  48265  snlindsntor  48334  ldepsnlinc  48371  elbigo2r  48420  elbigolo1  48424  itcovalt2  48544  mof0  48693  isnrm4  48776  iscnrm3r  48793  iscnrm4  48799  lubsscl  48805  glbsscl  48806  ipolubdm  48832  ipoglbdm  48835  setrecseq  49200  setrec2fun  49207  setrec2lem2  49209