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  914  19.23t  2211  axc14  2471  mojust  2542  mof  2566  eu6lem  2576  nfabdwOLD  2933  2gencl  3534  3gencl  3535  vtocl2gf  3584  vtocl3gf  3585  vtocl2g  3586  vtocl3g  3587  vtocl2ga  3590  vtocl2gaf  3591  vtocl3gaf  3593  vtocl3ga  3595  vtocl4g  3598  vtocl4ga  3599  eqeu  3728  mo2icl  3736  euind  3746  reu7  3754  reuind  3775  sbctt  3880  sbccomlem  3891  reu8nf  3899  sbcnestgfw  4444  sbcnestgf  4449  r19.36zv  4530  dedth2h  4607  dedth3h  4608  dedth4h  4609  reusngf  4696  reuprg0  4727  preq12bg  4878  elint  4976  elintrabg  4985  intab  5002  axrep1  5304  axreplem  5305  axrep2  5306  axrep6g  5311  bm1.3ii  5320  reusv3  5423  poclOLD  5616  swopolem  5618  solin  5634  freq1  5667  frminex  5679  vtoclr  5763  2optocl  5795  3optocl  5796  raliunxp  5864  resieq  6020  iss  6064  cnveqb  6227  reu3op  6323  reuop  6324  dfpo2  6327  preddowncl  6364  funmoOLD  6594  funimaexgOLD  6665  fnbrfvb  6973  fvelimab  6994  fvmptss  7041  fmptco  7163  fprg  7189  fnressn  7192  fressnfv  7194  isoselem  7377  ovg  7615  caovcan  7654  caovordig  7655  caovord  7661  tfisi  7896  tfindsg  7898  tfinds2  7901  tfinds3  7902  dfom2  7905  elom  7906  findsg  7937  finds2  7938  f1o2ndf1  8163  poxp  8169  fnse  8174  xpord3inddlem  8195  soseq  8200  fpr3g  8326  frrlem12  8338  fpr2a  8343  wfr3g  8363  wfrlem4OLD  8368  smoeq  8406  smores  8408  smogt  8423  tfrlem1  8432  tfr3  8455  oaordi  8602  oeordi  8643  oeoa  8653  oeoe  8655  nnacl  8667  nnmcl  8668  nnecl  8669  nnacom  8673  nnaordi  8674  nnawordi  8677  nnaass  8678  nndi  8679  nnmass  8680  nnmsucr  8681  nnmcom  8682  nnmordi  8687  naddssim  8741  naddoa  8758  2ecoptocl  8866  3ecoptocl  8867  undifixp  8992  xpdom2g  9134  findcard2  9230  unfi  9238  ssfi  9240  fnfi  9244  fodomfi  9378  imafiOLD  9382  xpfiOLD  9387  fodomfiOLD  9398  finsschain  9429  marypha1lem  9502  marypha1  9503  supeq1  9514  ordiso2  9584  ordtypelem7  9593  wemaplem1  9615  inf3lem2  9698  inf3lem5  9701  infdiffi  9727  cantnfval2  9738  cantnfle  9740  cantnfp1lem3  9749  oemapval  9752  cantnflem1  9758  cantnf  9762  wemapwe  9766  cnfcom  9769  cnfcom3clem  9774  ttrclss  9789  ttrclselem2  9795  tz9.1  9798  frr3g  9825  frr2  9829  r1pwALT  9915  cplem2  9959  karden  9964  updjud  10003  infxpenc2lem2  10089  fseqenlem1  10093  dfac8clem  10101  alephinit  10164  dfac4  10191  dfac5lem5  10196  dfac2a  10199  dfac2b  10200  dfacacn  10211  dfac12lem3  10215  kmlem2  10221  kmlem13  10232  nnadju  10267  ackbij1lem16  10303  sornom  10346  infpssrlem4  10375  fin23lem14  10402  fin23lem32  10413  fin23lem34  10415  fin23lem36  10417  isf32lem1  10422  isf32lem2  10423  axcc2lem  10505  axcc3  10507  axcclem  10526  zornn0g  10574  ttukeylem5  10582  ttukeylem6  10583  axrepnd  10663  axpowndlem3  10668  zfcndrep  10683  fpwwe2lem7  10706  pwfseqlem3  10729  wunr1om  10788  wunfi  10790  tskr1om  10836  ingru  10884  grudomon  10886  axgroth3  10900  axgroth4  10901  nqereu  10998  mulcanenq  11029  elnp  11056  elnpi  11057  prlem934  11102  infm3  12254  nnindd  12313  nnaddcl  12316  nnmulcl  12317  nnne0  12327  peano5uzi  12732  uzind2  12736  nn0indd  12740  zindd  12744  fzindd  12745  eluzaddOLD  12938  uzaddcl  12969  uzwo  12976  indstr  12981  zmax  13010  xmulasslem  13347  xrsupsslem  13369  xrinfmsslem  13370  xrsupss  13371  xrinfmss  13372  flval2  13865  om2uzlti  14001  uzrdgfni  14009  rabssnn0fi  14037  mptnn0fsupp  14048  seqcl2  14071  seqfveq2  14075  seqshft2  14079  monoord  14083  seqsplit  14086  seqcaopr3  14088  seqf1olem2a  14091  seqf1o  14094  seqid2  14099  seqhomo  14100  ser1const  14109  expcllem  14123  expeq0  14143  mulexp  14152  expadd  14155  expmul  14158  expmordi  14217  leexp2r  14224  leexp1a  14225  bernneq  14278  modexp  14287  facdiv  14336  faclbnd  14339  faclbnd4lem4  14345  hashgadd  14426  hashxp  14483  hashmap  14484  hashf1lem2  14505  hashf1  14506  seqcoll  14513  wrdind  14770  wrd2ind  14771  pfxccatin12lem3  14780  cshweqrep  14869  2cshwcshw  14874  relexp0g  15071  relexpsucnnr  15074  relexpsucnnl  15079  relexpcnv  15084  relexpnndm  15090  relexpaddnn  15100  rtrclreclem1  15106  dfrtrclrec2  15107  rtrclreclem2  15108  rtrclreclem4  15110  dfrtrcl2  15111  relexpind  15113  reusq0  15511  rlim  15541  rlim2  15542  rlim0  15554  rlim0lt  15555  rlimi  15559  ello12r  15563  ello1mpt  15567  ello1d  15569  elo12r  15574  lo1o1  15578  o1lo1  15583  lo1res  15605  climshft  15622  o1compt  15633  rlimo1  15663  lo1add  15673  lo1mul  15674  rlimdiv  15694  climub  15710  climserle  15711  caucvgrlem  15721  caurcvgr  15722  iseraltlem2  15731  summolem2a  15763  sumss  15772  fsum2d  15819  fsumabs  15849  fsumrlim  15859  fsumo1  15860  fsumiun  15869  binom  15878  climcndslem1  15897  climcndslem2  15898  cvgrat  15931  clim2prod  15936  prodfn0  15942  prodfrec  15943  ntrivcvgfvn0  15947  prodmolem2a  15982  fprodabs  16022  fprodn0  16027  fprod2d  16029  binomfallfac  16089  bpolycl  16100  bpolydif  16103  fprodefsum  16143  demoivreALT  16249  ruclem8  16285  ruclem9  16286  dvdsle  16358  dvdsfac  16374  divalglem7  16447  bitsinv1  16488  sadcadd  16504  sadadd2  16506  saddisjlem  16510  smuval2  16528  smupvallem  16529  smu01lem  16531  smupval  16534  smueqlem  16536  smumullem  16538  bezoutlem4  16589  dfgcd2  16593  rplpwr  16605  nn0seqcvgd  16617  seq1st  16618  alginv  16622  algcvga  16626  algfx  16627  lcmf  16680  prmind2  16732  prmdvdsexp  16762  prmfac1  16767  reumodprminv  16851  pcmpt  16939  pcfac  16946  prmpwdvds  16951  prmreclem4  16966  vdwlem10  17037  ramval  17055  ramcl  17076  cshwrepswhash1  17150  prmlem1a  17154  imasleval  17601  ismre  17648  mreexexd  17706  lubprop  18428  lublecllem  18430  glbprop  18441  joinlem  18453  meetlem  18467  poslubmo  18481  posglbmo  18482  poslubd  18483  isglbd  18579  lubun  18585  mndind  18863  frmdgsum  18897  mulgnnass  19149  mhmmulg  19155  gsumwrev  19409  gsmsymgrfix  19470  gsmsymgreq  19474  psgnunilem3  19538  sylow1lem1  19640  efginvrel2  19769  efgsrel  19776  efgredlemd  19786  efgredlem  19789  efgred  19790  efgrelexlemb  19792  gsum2dlem2  20013  gsumcom2  20017  ablfac1eulem  20116  pgpfac1lem2  20119  pgpfac1lem5  20123  pgpfac1  20124  pgpfac  20128  srgmulgass  20244  srgpcomp  20245  srgbinom  20258  isdomn2OLD  20734  isdomn3  20737  lmodvsmmulgdi  20917  cnfldexp  21440  islindf4  21881  assamulgscm  21944  mplcoe1  22078  mplcoe3  22079  mplcoe5  22081  gsummoncoe1  22333  dmatval  22519  dmatel  22520  dmatmulcl  22527  pmatcoe1fsupp  22728  decpmataa0  22795  decpmatmulsumfsupp  22800  pmatcollpw2lem  22804  pm2mpmhmlem1  22845  fiinopn  22928  mretopd  23121  neiptoptop  23160  cnpfval  23263  iscnp3  23273  tgcn  23281  lmbr  23287  lmbr2  23288  lmbrf  23289  lmss  23327  ishaus  23351  hausnei2  23382  t1sep2  23398  fiuncmp  23433  dfconn2  23448  1stcfb  23474  2ndc1stc  23480  1stcrest  23482  1stcelcls  23490  1stccn  23492  lly1stc  23525  elkgen  23565  kgencn  23585  tx1stc  23679  xkopt  23684  cnmptcom  23707  isr0  23766  r0sep  23777  ptcmpfi  23842  isfildlem  23886  rnelfm  23982  fbflim  24005  flimrest  24012  isflf  24022  flffbas  24024  lmflf  24034  fclsrest  24053  isfcf  24063  cnextfvval  24094  tmdgsum  24124  eltsms  24162  tsmsi  24163  tsmsgsum  24168  tsmssubm  24172  tsmsres  24173  tsmsf1o  24174  isust  24233  isucn  24308  isucn2  24309  ucnima  24311  imasdsf1olem  24404  metss  24542  met1stc  24555  metcnp  24575  metcnpi  24578  metcnpi2  24579  metucn  24605  xrge0tsms  24875  fsumcn  24913  elcncf  24934  cncfi  24939  rescncf  24942  cncfco  24952  caucfil  25336  equivcau  25353  caubl  25361  caublcls  25362  ovolgelb  25534  ovolunlem1a  25550  ovolicc2lem3  25573  voliunlem1  25604  voliunlem3  25606  volsuplem  25609  volsup  25610  dyadmax  25652  vitali  25667  itg2leub  25789  itgfsum  25882  dvnadd  25985  dvnres  25987  cpnord  25991  dvnfre  26010  dvmptfsum  26033  dvferm1  26043  dvferm2  26045  rolle  26048  dvlip  26052  c1lip1  26056  lhop1  26073  deg1leb  26154  ply1divex  26196  fta1g  26229  plyco  26300  dgrcolem1  26333  dgrco  26335  dvnply2  26347  plydivex  26357  aalioulem2  26393  aalioulem3  26394  aalioulem5  26396  aaliou3lem2  26403  dvntaylp  26431  taylthlem1  26433  ulmdvlem3  26463  abelthlem9  26502  cxpmul2  26749  scvxcvx  27047  jensenlem2  27049  jensen  27050  wilthlem3  27131  perfectlem2  27292  bcmono  27339  bposlem5  27350  lgsquad2lem2  27447  addsq2reu  27502  2sqreulem1  27508  2sqreunnlem1  27511  dchrisumlem1  27551  dchrisum0flb  27572  pntpbnd1  27648  pntlemf  27667  qabvle  27687  qabvexp  27688  ostthlem2  27690  ostth2lem2  27696  nosupcbv  27765  nosupno  27766  nosupdm  27767  nosupfv  27769  nosupres  27770  nosupbnd1lem1  27771  nosupbnd1lem3  27773  nosupbnd1lem5  27775  noinfcbv  27780  noinfno  27781  noinfdm  27782  noinffv  27784  noinfres  27785  noinfbnd1lem3  27788  noinfbnd1lem5  27790  eqscut2  27869  addsproplem1  28020  addsprop  28027  negsunif  28105  mulsproplem9  28168  ssltmul2  28192  precsexlem8  28256  precsexlem9  28257  precsexlem11  28259  noseqind  28316  om2noseqrdg  28328  noseqrdgfn  28330  n0addscl  28365  n0mulscl  28366  peano5uzs  28408  expscl  28431  expsne0  28432  expsgt0  28433  pw2cut  28438  tgcgr4  28557  usgr2pth  29800  wlkiswwlks2lem4  29905  wlkiswwlks2  29908  rusgrnumwwlk  30008  clwlkclwwlklem2a  30030  clwlkclwwlklem1  30031  clwlkclwwlkfo  30041  eupth2  30271  frgr3vlem1  30305  3vfriswmgrlem  30309  3vfriswmgr  30310  wlkl0  30399  numclwlk2lem2f1o  30411  isplig  30508  isnvlem  30642  nvi  30646  nmoubi  30804  nmounbi  30808  nmblolbi  30832  ipasslem1  30863  ipassi  30873  hlim2  31224  pjhth  31425  spansni  31589  elspansn2  31599  pjige0  31723  pjcjt2  31724  pjopyth  31752  elcnop  31889  elcnfn  31914  nmopub  31940  cnopc  31945  nmfnleub  31957  elnlfn  31960  cnfnc  31962  nmbdoplb  32057  nmcexi  32058  nmcoplb  32062  lnfnmul  32080  nmbdfnlb  32082  nmcfnlb  32086  pjss2coi  32196  pjssmi  32197  isst  32245  ishst  32246  stcltr1i  32306  mdbr  32326  dmdbr  32331  mddmd2  32341  mdslmd1lem3  32359  mdslmd1lem4  32360  elat2  32372  atcvat2  32421  cdj1i  32465  iuninc  32583  fmptcof2  32675  nn0min  32824  wrdt2ind  32920  ismnt  32956  xrge0tsmsd  33041  isomnd  33051  omndadd  33056  cyc3genpm  33145  isarchi2  33165  archirng  33168  archiexdiv  33170  archiabl  33178  domnprodn0  33247  isorng  33294  ofldchr  33309  islbs5  33373  unitprodclb  33382  mxidlval  33454  1arithidom  33530  1arithufdlem3  33539  crefeq  33791  nexple  33973  esumfzf  34033  issiga  34076  isrnsiga  34077  isldsys  34120  ismeas  34163  isrnmeas  34164  measiun  34182  eulerpartlemn  34346  sseqp1  34360  rrvsum  34419  signsply0  34528  signstfvc  34551  bnj941  34748  bnj106  34844  bnj155  34855  bnj590  34886  bnj591  34887  bnj849  34901  bnj893  34904  bnj944  34914  bnj1128  34966  gblacfnacd  35075  subfacp1lem6  35153  erdszelem8  35166  issconn  35194  cvmliftlem7  35259  cvmliftlem10  35262  cvmlift3lem2  35288  satfsschain  35332  satfrel  35335  satfdm  35337  satfrnmapom  35338  fmlafvel  35353  satffun  35377  mrsubvrs  35490  mclsssvlem  35530  mclsval  35531  mclsax  35537  mclsind  35538  shftvalg  35694  bccolsum  35701  iprodefisumlem  35702  faclimlem1  35705  rdgprc  35758  sbequbidv  36180  cbvsbdavw  36220  fveleq  36417  unblimceq0  36473  bj-ax12  36623  bj-bm1.3ii  37030  rdgeqoa  37336  finxpreclem6  37362  domalom  37370  ralssiun  37373  wl-sblimt  37502  wl-sbhbt  37508  wl-2sb6d  37512  wl-mo2df  37524  wl-mo2t  37529  poimirlem2  37582  poimirlem25  37605  poimirlem28  37608  poimirlem31  37611  heicant  37615  mbfresfi  37626  itg2gt0cn  37635  sdclem2  37702  fdc  37705  seqpo  37707  incsequz  37708  mettrifi  37717  prdsbnd2  37755  heiborlem4  37774  bfplem1  37782  iscringd  37958  maxidlval  37999  igenval2  38026  iss2  38300  elrefrels3  38475  ax12eq  38897  ax12el  38898  ax12indalem  38901  ax12inda2ALT  38902  ax12inda  38904  ax12v2-o  38905  riotasvd  38912  isopos  39136  isat3  39263  ishlat1  39308  glbconN  39333  glbconNOLD  39334  ispsubsp  39702  isldil  40067  isltrn  40076  isdilN  40111  trlval  40119  cdleme27b  40325  cdleme29b  40332  cdleme31sn1  40338  cdleme31sn1c  40345  cdleme40v  40426  cdlemk36  40870  cdlemkid5  40892  cdlemn11pre  41167  dihord2pre  41182  islpolN  41440  hdmapffval  41783  hdmapfval  41784  hdmapval2lem  41788  uzindd  41933  sticksstones1  42103  sticksstones2  42104  sticksstones3  42105  sticksstones8  42110  sticksstones10  42112  sticksstones11  42113  sticksstones12a  42114  sticksstones15  42118  indstrd  42150  unitscyglem3  42154  nnaddcom  42257  nnadddir  42259  nnmulcom  42261  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  43130  unielss  43179  onsucf1lem  43231  cantnfresb  43286  onmcl  43293  naddonnn  43357  elmapintrab  43538  elmapintab  43558  cnvcnvintabd  43562  eliunov2  43641  relexpxpnnidm  43665  relexpiidm  43666  relexpss1d  43667  iunrelexpmin1  43670  relexpmulnn  43671  iunrelexpmin2  43674  relexp0a  43678  trclimalb2  43688  clsk3nimkb  44002  ntrclsiso  44029  ntrclskb  44031  ntrneiiso  44053  ntrneix2  44055  ntrneixb  44057  gneispace2  44094  gneispacess2  44108  mnuunid  44246  dvgrat  44281  pm14.122b  44392  fnchoice  44929  fiiuncl  44967  ssinc  44989  ssdec  44990  wessf1ornlem  45092  dmrelrnrel  45133  fperiodmullem  45218  monoordxrv  45397  fmul01  45501  fmuldfeq  45504  climsuselem1  45528  climinff  45532  ellimcabssub0  45538  limcleqr  45565  addlimc  45569  0ellimcdiv  45570  limclner  45572  limsupref  45606  limsupub  45625  limsupmnf  45642  limsupre2lem  45645  limsupre2  45646  limsupre2mpt  45651  limsupre3lem  45653  limsupre3  45654  limsupre3mpt  45655  xlimbr  45748  cnrefiisplem  45750  dvnmptdivc  45859  dvnmptconst  45862  dvnmul  45864  iblspltprt  45894  itgspltprt  45900  stoweidlem2  45923  stoweidlem3  45924  stoweidlem17  45938  stoweidlem19  45940  stoweidlem21  45942  stoweidlem26  45947  fourierdlem42  46070  issal  46235  ismea  46372  isome  46415  carageniuncllem1  46442  caratheodorylem1  46447  2reu8i  47028  2reuimp0  47029  funressndmafv2rn  47138  2ffzoeq  47242  smonoord  47245  fargshiftf1  47315  ichnfimlem  47337  paireqne  47385  reupr  47396  reuopreuprim  47400  perfectALTVlem2  47596  grimcnv  47763  lmodvsmdi  48107  dmatALTval  48129  dmatALTbasel  48131  snlindsntor  48200  ldepsnlinc  48237  elbigo2r  48287  elbigolo1  48291  itcovalt2  48411  mof0  48551  isnrm4  48610  iscnrm3r  48628  iscnrm4  48634  lubsscl  48640  glbsscl  48641  ipolubdm  48659  ipoglbdm  48662  setrecseq  48777  setrec2fun  48784  setrec2lem2  48786