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  2207  axc14  2465  mojust  2536  mof  2560  eu6lem  2570  2gencl  3521  3gencl  3522  vtocl2gf  3571  vtocl3gf  3572  vtocl2g  3573  vtocl3g  3574  vtocl2ga  3577  vtocl2gaf  3578  vtocl3gaf  3580  vtocl3ga  3582  vtocl4g  3584  vtocl4ga  3585  eqeu  3714  mo2icl  3722  euind  3732  reu7  3740  reuind  3761  sbctt  3866  sbccomlem  3877  reu8nf  3885  sbcnestgfw  4426  sbcnestgf  4431  r19.36zv  4512  dedth2h  4589  dedth3h  4590  dedth4h  4591  reusngf  4678  reuprg0  4706  preq12bg  4857  elint  4956  elintrabg  4965  intab  4982  axrep1  5285  axreplem  5286  axrep2  5287  axrep6g  5295  bm1.3iiOLD  5307  reusv3  5410  swopolem  5606  solin  5622  freq1  5655  frminex  5667  vtoclr  5751  2optocl  5783  3optocl  5784  raliunxp  5852  resieq  6010  iss  6054  cnveqb  6217  reu3op  6313  reuop  6314  dfpo2  6317  preddowncl  6354  funmoOLD  6583  funimaexgOLD  6654  fnbrfvb  6959  fvelimab  6980  fvmptss  7027  fmptco  7148  fprg  7174  fnressn  7177  fressnfv  7179  isoselem  7360  ovg  7597  caovcan  7636  caovordig  7637  caovord  7643  tfisi  7879  tfindsg  7881  tfinds2  7884  tfinds3  7885  dfom2  7888  elom  7889  findsg  7919  finds2  7920  f1o2ndf1  8145  poxp  8151  fnse  8156  xpord3inddlem  8177  soseq  8182  fpr3g  8308  frrlem12  8320  fpr2a  8325  wfr3g  8345  wfrlem4OLD  8350  smoeq  8388  smores  8390  smogt  8405  tfrlem1  8414  tfr3  8437  oaordi  8582  oeordi  8623  oeoa  8633  oeoe  8635  nnacl  8647  nnmcl  8648  nnecl  8649  nnacom  8653  nnaordi  8654  nnawordi  8657  nnaass  8658  nndi  8659  nnmass  8660  nnmsucr  8661  nnmcom  8662  nnmordi  8667  naddssim  8721  naddoa  8738  2ecoptocl  8846  3ecoptocl  8847  undifixp  8972  xpdom2g  9106  findcard2  9202  unfi  9209  ssfi  9211  fnfi  9215  fodomfi  9347  imafiOLD  9351  xpfiOLD  9356  fodomfiOLD  9367  finsschain  9396  marypha1lem  9470  marypha1  9471  supeq1  9482  ordiso2  9552  ordtypelem7  9561  wemaplem1  9583  inf3lem2  9666  inf3lem5  9669  infdiffi  9695  cantnfval2  9706  cantnfle  9708  cantnfp1lem3  9717  oemapval  9720  cantnflem1  9726  cantnf  9730  wemapwe  9734  cnfcom  9737  cnfcom3clem  9742  ttrclss  9757  ttrclselem2  9763  tz9.1  9766  frr3g  9793  frr2  9797  r1pwALT  9883  cplem2  9927  karden  9932  updjud  9971  infxpenc2lem2  10057  fseqenlem1  10061  dfac8clem  10069  alephinit  10132  dfac4  10159  dfac5lem5  10164  dfac2a  10167  dfac2b  10168  dfacacn  10179  dfac12lem3  10183  kmlem2  10189  kmlem13  10200  nnadju  10235  ackbij1lem16  10271  sornom  10314  infpssrlem4  10343  fin23lem14  10370  fin23lem32  10381  fin23lem34  10383  fin23lem36  10385  isf32lem1  10390  isf32lem2  10391  axcc2lem  10473  axcc3  10475  axcclem  10494  zornn0g  10542  ttukeylem5  10550  ttukeylem6  10551  axrepnd  10631  axpowndlem3  10636  zfcndrep  10651  fpwwe2lem7  10674  pwfseqlem3  10697  wunr1om  10756  wunfi  10758  tskr1om  10804  ingru  10852  grudomon  10854  axgroth3  10868  axgroth4  10869  nqereu  10966  mulcanenq  10997  elnp  11024  elnpi  11025  prlem934  11070  infm3  12224  nnindd  12283  nnaddcl  12286  nnmulcl  12287  nnne0  12297  peano5uzi  12704  uzind2  12708  nn0indd  12712  zindd  12716  fzindd  12717  eluzaddOLD  12910  uzaddcl  12943  uzwo  12950  indstr  12955  zmax  12984  xmulasslem  13323  xrsupsslem  13345  xrinfmsslem  13346  xrsupss  13347  xrinfmss  13348  flval2  13850  om2uzlti  13987  uzrdgfni  13995  rabssnn0fi  14023  mptnn0fsupp  14034  seqcl2  14057  seqfveq2  14061  seqshft2  14065  monoord  14069  seqsplit  14072  seqcaopr3  14074  seqf1olem2a  14077  seqf1o  14080  seqid2  14085  seqhomo  14086  ser1const  14095  expcllem  14109  expeq0  14129  mulexp  14138  expadd  14141  expmul  14144  expmordi  14203  leexp2r  14210  leexp1a  14211  bernneq  14264  modexp  14273  facdiv  14322  faclbnd  14325  faclbnd4lem4  14331  hashgadd  14412  hashxp  14469  hashmap  14470  hashf1lem2  14491  hashf1  14492  seqcoll  14499  wrdind  14756  wrd2ind  14757  pfxccatin12lem3  14766  cshweqrep  14855  2cshwcshw  14860  relexp0g  15057  relexpsucnnr  15060  relexpsucnnl  15065  relexpcnv  15070  relexpnndm  15076  relexpaddnn  15086  rtrclreclem1  15092  dfrtrclrec2  15093  rtrclreclem2  15094  rtrclreclem4  15096  dfrtrcl2  15097  relexpind  15099  reusq0  15497  rlim  15527  rlim2  15528  rlim0  15540  rlim0lt  15541  rlimi  15545  ello12r  15549  ello1mpt  15553  ello1d  15555  elo12r  15560  lo1o1  15564  o1lo1  15569  lo1res  15591  climshft  15608  o1compt  15619  rlimo1  15649  lo1add  15659  lo1mul  15660  rlimdiv  15678  climub  15694  climserle  15695  caucvgrlem  15705  caurcvgr  15706  iseraltlem2  15715  summolem2a  15747  sumss  15756  fsum2d  15803  fsumabs  15833  fsumrlim  15843  fsumo1  15844  fsumiun  15853  binom  15862  climcndslem1  15881  climcndslem2  15882  cvgrat  15915  clim2prod  15920  prodfn0  15926  prodfrec  15927  ntrivcvgfvn0  15931  prodmolem2a  15966  fprodabs  16006  fprodn0  16011  fprod2d  16013  binomfallfac  16073  bpolycl  16084  bpolydif  16087  fprodefsum  16127  demoivreALT  16233  ruclem8  16269  ruclem9  16270  dvdsle  16343  dvdsfac  16359  divalglem7  16432  bitsinv1  16475  sadcadd  16491  sadadd2  16493  saddisjlem  16497  smuval2  16515  smupvallem  16516  smu01lem  16518  smupval  16521  smueqlem  16523  smumullem  16525  bezoutlem4  16575  dfgcd2  16579  rplpwr  16591  nn0seqcvgd  16603  seq1st  16604  alginv  16608  algcvga  16612  algfx  16613  lcmf  16666  prmind2  16718  prmdvdsexp  16748  prmfac1  16753  reumodprminv  16837  pcmpt  16925  pcfac  16932  prmpwdvds  16937  prmreclem4  16952  vdwlem10  17023  ramval  17041  ramcl  17062  cshwrepswhash1  17136  prmlem1a  17140  imasleval  17587  ismre  17634  mreexexd  17692  lubprop  18415  lublecllem  18417  glbprop  18428  joinlem  18440  meetlem  18454  poslubmo  18468  posglbmo  18469  poslubd  18470  isglbd  18566  lubun  18572  mndind  18853  frmdgsum  18887  mulgnnass  19139  mhmmulg  19145  gsumwrev  19399  gsmsymgrfix  19460  gsmsymgreq  19464  psgnunilem3  19528  sylow1lem1  19630  efginvrel2  19759  efgsrel  19766  efgredlemd  19776  efgredlem  19779  efgred  19780  efgrelexlemb  19782  gsum2dlem2  20003  gsumcom2  20007  ablfac1eulem  20106  pgpfac1lem2  20109  pgpfac1lem5  20113  pgpfac1  20114  pgpfac  20118  srgmulgass  20234  srgpcomp  20235  srgbinom  20248  isdomn2OLD  20728  isdomn3  20731  lmodvsmmulgdi  20911  cnfldexp  21434  islindf4  21875  assamulgscm  21938  mplcoe1  22072  mplcoe3  22073  mplcoe5  22075  gsummoncoe1  22327  dmatval  22513  dmatel  22514  dmatmulcl  22521  pmatcoe1fsupp  22722  decpmataa0  22789  decpmatmulsumfsupp  22794  pmatcollpw2lem  22798  pm2mpmhmlem1  22839  fiinopn  22922  mretopd  23115  neiptoptop  23154  cnpfval  23257  iscnp3  23267  tgcn  23275  lmbr  23281  lmbr2  23282  lmbrf  23283  lmss  23321  ishaus  23345  hausnei2  23376  t1sep2  23392  fiuncmp  23427  dfconn2  23442  1stcfb  23468  2ndc1stc  23474  1stcrest  23476  1stcelcls  23484  1stccn  23486  lly1stc  23519  elkgen  23559  kgencn  23579  tx1stc  23673  xkopt  23678  cnmptcom  23701  isr0  23760  r0sep  23771  ptcmpfi  23836  isfildlem  23880  rnelfm  23976  fbflim  23999  flimrest  24006  isflf  24016  flffbas  24018  lmflf  24028  fclsrest  24047  isfcf  24057  cnextfvval  24088  tmdgsum  24118  eltsms  24156  tsmsi  24157  tsmsgsum  24162  tsmssubm  24166  tsmsres  24167  tsmsf1o  24168  isust  24227  isucn  24302  isucn2  24303  ucnima  24305  imasdsf1olem  24398  metss  24536  met1stc  24549  metcnp  24569  metcnpi  24572  metcnpi2  24573  metucn  24599  xrge0tsms  24869  fsumcn  24907  elcncf  24928  cncfi  24933  rescncf  24936  cncfco  24946  caucfil  25330  equivcau  25347  caubl  25355  caublcls  25356  ovolgelb  25528  ovolunlem1a  25544  ovolicc2lem3  25567  voliunlem1  25598  voliunlem3  25600  volsuplem  25603  volsup  25604  dyadmax  25646  vitali  25661  itg2leub  25783  itgfsum  25876  dvnadd  25979  dvnres  25981  cpnord  25985  dvnfre  26004  dvmptfsum  26027  dvferm1  26037  dvferm2  26039  rolle  26042  dvlip  26046  c1lip1  26050  lhop1  26067  deg1leb  26148  ply1divex  26190  fta1g  26223  plyco  26294  dgrcolem1  26327  dgrco  26329  dvnply2  26343  plydivex  26353  aalioulem2  26389  aalioulem3  26390  aalioulem5  26392  aaliou3lem2  26399  dvntaylp  26427  taylthlem1  26429  ulmdvlem3  26459  abelthlem9  26498  cxpmul2  26745  scvxcvx  27043  jensenlem2  27045  jensen  27046  wilthlem3  27127  perfectlem2  27288  bcmono  27335  bposlem5  27346  lgsquad2lem2  27443  addsq2reu  27498  2sqreulem1  27504  2sqreunnlem1  27507  dchrisumlem1  27547  dchrisum0flb  27568  pntpbnd1  27644  pntlemf  27663  qabvle  27683  qabvexp  27684  ostthlem2  27686  ostth2lem2  27692  nosupcbv  27761  nosupno  27762  nosupdm  27763  nosupfv  27765  nosupres  27766  nosupbnd1lem1  27767  nosupbnd1lem3  27769  nosupbnd1lem5  27771  noinfcbv  27776  noinfno  27777  noinfdm  27778  noinffv  27780  noinfres  27781  noinfbnd1lem3  27784  noinfbnd1lem5  27786  eqscut2  27865  addsproplem1  28016  addsprop  28023  negsunif  28101  mulsproplem9  28164  ssltmul2  28188  precsexlem8  28252  precsexlem9  28253  precsexlem11  28255  noseqind  28312  om2noseqrdg  28324  noseqrdgfn  28326  n0addscl  28361  n0mulscl  28362  peano5uzs  28404  expscl  28427  expsne0  28428  expsgt0  28429  pw2cut  28434  tgcgr4  28553  usgr2pth  29796  wlkiswwlks2lem4  29901  wlkiswwlks2  29904  rusgrnumwwlk  30004  clwlkclwwlklem2a  30026  clwlkclwwlklem1  30027  clwlkclwwlkfo  30037  eupth2  30267  frgr3vlem1  30301  3vfriswmgrlem  30305  3vfriswmgr  30306  wlkl0  30395  numclwlk2lem2f1o  30407  isplig  30504  isnvlem  30638  nvi  30642  nmoubi  30800  nmounbi  30804  nmblolbi  30828  ipasslem1  30859  ipassi  30869  hlim2  31220  pjhth  31421  spansni  31585  elspansn2  31595  pjige0  31719  pjcjt2  31720  pjopyth  31748  elcnop  31885  elcnfn  31910  nmopub  31936  cnopc  31941  nmfnleub  31953  elnlfn  31956  cnfnc  31958  nmbdoplb  32053  nmcexi  32054  nmcoplb  32058  lnfnmul  32076  nmbdfnlb  32078  nmcfnlb  32082  pjss2coi  32192  pjssmi  32193  isst  32241  ishst  32242  stcltr1i  32302  mdbr  32322  dmdbr  32327  mddmd2  32337  mdslmd1lem3  32355  mdslmd1lem4  32356  elat2  32368  atcvat2  32417  cdj1i  32461  iuninc  32580  fmptcof2  32673  nn0min  32826  wrdt2ind  32922  ismnt  32957  xrge0tsmsd  33047  gsumwun  33050  isomnd  33060  omndadd  33065  cyc3genpm  33154  isarchi2  33174  archirng  33177  archiexdiv  33179  archiabl  33187  domnprodn0  33261  isorng  33308  ofldchr  33323  islbs5  33387  unitprodclb  33396  mxidlval  33468  1arithidom  33544  1arithufdlem3  33553  crefeq  33805  nexple  33989  esumfzf  34049  issiga  34092  isrnsiga  34093  isldsys  34136  ismeas  34179  isrnmeas  34180  measiun  34198  eulerpartlemn  34362  sseqp1  34376  rrvsum  34435  signsply0  34544  signstfvc  34567  bnj941  34764  bnj106  34860  bnj155  34871  bnj590  34902  bnj591  34903  bnj849  34917  bnj893  34920  bnj944  34930  bnj1128  34982  gblacfnacd  35091  subfacp1lem6  35169  erdszelem8  35182  issconn  35210  cvmliftlem7  35275  cvmliftlem10  35278  cvmlift3lem2  35304  satfsschain  35348  satfrel  35351  satfdm  35353  satfrnmapom  35354  fmlafvel  35369  satffun  35393  mrsubvrs  35506  mclsssvlem  35546  mclsval  35547  mclsax  35553  mclsind  35554  shftvalg  35711  bccolsum  35718  iprodefisumlem  35719  faclimlem1  35722  rdgprc  35775  sbequbidv  36196  cbvsbdavw  36236  fveleq  36433  unblimceq0  36489  bj-ax12  36639  bj-bm1.3ii  37046  rdgeqoa  37352  finxpreclem6  37378  domalom  37386  ralssiun  37389  wl-ax12v2cl  37486  wl-sblimt  37528  wl-sbhbt  37534  wl-2sb6d  37538  wl-mo2df  37550  wl-mo2t  37555  poimirlem2  37608  poimirlem25  37631  poimirlem28  37634  poimirlem31  37637  heicant  37641  mbfresfi  37652  itg2gt0cn  37661  sdclem2  37728  fdc  37731  seqpo  37733  incsequz  37734  mettrifi  37743  prdsbnd2  37781  heiborlem4  37800  bfplem1  37808  iscringd  37984  maxidlval  38025  igenval2  38052  iss2  38325  elrefrels3  38500  ax12eq  38922  ax12el  38923  ax12indalem  38926  ax12inda2ALT  38927  ax12inda  38929  ax12v2-o  38930  riotasvd  38937  isopos  39161  isat3  39288  ishlat1  39333  glbconN  39358  glbconNOLD  39359  ispsubsp  39727  isldil  40092  isltrn  40101  isdilN  40136  trlval  40144  cdleme27b  40350  cdleme29b  40357  cdleme31sn1  40363  cdleme31sn1c  40370  cdleme40v  40451  cdlemk36  40895  cdlemkid5  40917  cdlemn11pre  41192  dihord2pre  41207  islpolN  41465  hdmapffval  41808  hdmapfval  41809  hdmapval2lem  41813  uzindd  41958  sticksstones1  42127  sticksstones2  42128  sticksstones3  42129  sticksstones8  42134  sticksstones10  42136  sticksstones11  42137  sticksstones12a  42138  sticksstones15  42142  indstrd  42174  unitscyglem3  42178  nnaddcom  42281  nnadddir  42283  nnmulcom  42285  eu6w  42662  ismrc  42688  incssnn0  42698  mzpexpmpt  42732  pell14qrexpclnn0  42853  monotuz  42929  rmxypos  42935  jm2.17a  42948  jm2.17b  42949  rmygeid  42952  jm2.18  42976  jm2.19lem3  42979  jm2.25  42987  jm2.15nn0  42991  jm2.16nn0  42992  wepwsolem  43030  aomclem8  43049  dfac11  43050  pwslnm  43082  lnr2i  43104  hbtlem5  43116  cnsrexpcl  43153  rngunsnply  43157  unielss  43206  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  44272  dvgrat  44307  pm14.122b  44418  prclaxpr  44947  fnchoice  44966  fiiuncl  45004  ssinc  45026  ssdec  45027  wessf1ornlem  45127  dmrelrnrel  45168  fperiodmullem  45253  monoordxrv  45431  fmul01  45535  fmuldfeq  45538  climsuselem1  45562  climinff  45566  ellimcabssub0  45572  limcleqr  45599  addlimc  45603  0ellimcdiv  45604  limclner  45606  limsupref  45640  limsupub  45659  limsupmnf  45676  limsupre2lem  45679  limsupre2  45680  limsupre2mpt  45685  limsupre3lem  45687  limsupre3  45688  limsupre3mpt  45689  xlimbr  45782  cnrefiisplem  45784  dvnmptdivc  45893  dvnmptconst  45896  dvnmul  45898  iblspltprt  45928  itgspltprt  45934  stoweidlem2  45957  stoweidlem3  45958  stoweidlem17  45972  stoweidlem19  45974  stoweidlem21  45976  stoweidlem26  45981  fourierdlem42  46104  issal  46269  ismea  46406  isome  46449  carageniuncllem1  46476  caratheodorylem1  46481  2reu8i  47062  2reuimp0  47063  funressndmafv2rn  47172  2ffzoeq  47276  smonoord  47295  fargshiftf1  47365  ichnfimlem  47387  paireqne  47435  reupr  47446  reuopreuprim  47450  perfectALTVlem2  47646  grimcnv  47816  lmodvsmdi  48223  dmatALTval  48245  dmatALTbasel  48247  snlindsntor  48316  ldepsnlinc  48353  elbigo2r  48402  elbigolo1  48406  itcovalt2  48526  mof0  48667  isnrm4  48726  iscnrm3r  48744  iscnrm4  48750  lubsscl  48756  glbsscl  48757  ipolubdm  48775  ipoglbdm  48778  setrecseq  48915  setrec2fun  48922  setrec2lem2  48924