Theorem imbi2d 342

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  imbi12d  346  imbi2  350  pm5.42  551  orbi2d  926  19.23t  2244  axc14  2493  mojust  2564  mof  2589  eu6lem  2599  2gencl  3495  3gencl  3496  vtocl2gf  3535  vtocl3gf  3536  vtocl2g  3537  vtocl3g  3538  vtocl2ga  3541  vtocl2gaf  3542  vtocl3gaf  3543  vtocl3ga  3544  vtocl4g  3545  vtocl4ga  3546  eqeu  3667  mo2icl  3675  euind  3685  reu7  3693  reuind  3714  sbctt  3811  sbccomlem  3820  reu8nf  3828  sbcnestgfw  4372  sbcnestgf  4377  r19.36zv  4463  dedth2h  4537  dedth3h  4538  dedth4h  4539  reusngf  4630  reuprg0  4658  preq12bg  4808  elint  4908  elintrabg  4916  intab  4933  axrep1  5225  axreplem  5226  axrep2  5227  axrep6g  5237  bm1.3iiOLD  5249  reusv3  5359  swopolem  5561  solin  5578  freq1  5610  frminex  5622  vtoclr  5706  2optocl  5739  3optocl  5740  raliunxp  5807  resieq  5972  iss  6020  cnveqb  6178  reu3op  6274  reuop  6275  dfpo2  6278  preddowncl  6314  fnbrfvb  6912  fvelimab  6934  fvmptss  6983  fmptco  7106  fprg  7133  fnressn  7136  fressnfv  7138  isoselem  7320  ovg  7556  caovcan  7595  caovordig  7596  caovord  7602  tfisi  7834  tfindsg  7836  tfinds2  7839  tfinds3  7840  dfom2  7843  elom  7844  findsg  7873  finds2  7874  resf1extb  7910  f1o2ndf1  8095  poxp  8102  fnse  8107  xpord3inddlem  8128  soseq  8133  fpr3g  8260  frrlem12  8272  fpr2a  8277  wfr3g  8294  smoeq  8315  smores  8317  smogt  8332  tfrlem1  8340  tfr3  8364  oaordi  8509  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  8650  naddoa  8667  2ecoptocl  8784  3ecoptocl  8785  undifixp  8910  xpdom2g  9039  findcard2  9127  unfi  9133  ssfi  9135  fnfi  9140  fodomfi  9250  imafiOLD  9254  finsschain  9296  marypha1lem  9373  marypha1  9374  supeq1  9385  ordiso2  9457  ordtypelem7  9466  wemaplem1  9488  inf3lem2  9578  inf3lem5  9581  infdiffi  9607  cantnfval2  9618  cantnfle  9620  cantnfp1lem3  9629  oemapval  9632  cantnflem1  9638  cantnf  9642  wemapwe  9646  cnfcom  9649  cnfcom3clem  9654  ttrclss  9669  ttrclselem2  9675  tz9.1  9678  frr3g  9708  frr2  9712  r1pwALT  9798  cplem2  9842  karden  9847  updjud  9886  infxpenc2lem2  9970  fseqenlem1  9974  dfac8clem  9982  alephinit  10045  dfac4  10072  dfac5lem5  10077  dfac2a  10080  dfac2b  10081  dfacacn  10092  dfac12lem3  10096  kmlem2  10102  kmlem13  10113  nnadju  10148  ackbij1lem16  10184  sornom  10228  infpssrlem4  10257  fin23lem14  10284  fin23lem32  10295  fin23lem34  10297  fin23lem36  10299  isf32lem1  10304  isf32lem2  10305  axcc2lem  10387  axcc3  10389  axcclem  10408  zornn0g  10456  ttukeylem5  10464  ttukeylem6  10465  axrepnd  10546  axpowndlem3  10551  zfcndrep  10566  fpwwe2lem7  10589  pwfseqlem3  10612  wunr1om  10671  wunfi  10673  tskr1om  10719  ingru  10767  grudomon  10769  axgroth3  10783  axgroth4  10784  nqereu  10881  mulcanenq  10912  elnp  10939  elnpi  10940  prlem934  10985  infm3  12145  nnindd  12224  nnaddcl  12227  nnmulcl  12228  nnaddcom  12231  nnne0  12241  nnadddir  12263  nnmulcom  12265  peano5uzi  12656  uzind2  12660  nn0indd  12664  zindd  12668  fzindd  12669  uzaddcl  12899  uzwo  12906  indstr  12911  zmax  12940  xmulasslem  13282  xrsupsslem  13304  xrinfmsslem  13305  xrsupss  13306  xrinfmss  13307  flval2  13818  om2uzlti  13957  uzrdgfni  13965  rabssnn0fi  13993  mptnn0fsupp  14004  seqcl2  14027  seqfveq2  14031  seqshft2  14035  monoord  14039  seqsplit  14042  seqcaopr3  14044  seqf1olem2a  14047  seqf1o  14050  seqid2  14055  seqhomo  14056  ser1const  14065  expcllem  14079  expeq0  14099  mulexp  14108  expadd  14111  expmul  14114  expmordi  14174  leexp2r  14181  leexp1a  14182  bernneq  14236  modexp  14245  facdiv  14294  faclbnd  14297  faclbnd4lem4  14303  hashgadd  14384  hashxp  14441  hashmap  14442  hashf1lem2  14463  hashf1  14464  seqcoll  14471  wrdind  14729  wrd2ind  14730  pfxccatin12lem3  14739  cshweqrep  14828  2cshwcshw  14832  relexp0g  15029  relexpsucnnr  15032  relexpsucnnl  15037  relexpcnv  15042  relexpnndm  15048  relexpaddnn  15058  rtrclreclem1  15064  dfrtrclrec2  15065  rtrclreclem2  15066  rtrclreclem4  15068  dfrtrcl2  15069  relexpind  15071  reusq0  15483  rlim  15513  rlim2  15514  rlim0  15526  rlim0lt  15527  rlimi  15531  ello12r  15535  ello1mpt  15539  ello1d  15541  elo12r  15546  lo1o1  15550  o1lo1  15555  lo1res  15577  climshft  15594  o1compt  15605  rlimo1  15635  lo1add  15645  lo1mul  15646  rlimdiv  15664  climub  15680  climserle  15681  caucvgrlem  15691  caurcvgr  15692  iseraltlem2  15701  summolem2a  15733  sumss  15742  fsum2d  15789  fsumabs  15820  fsumrlim  15830  fsumo1  15831  fsumiun  15840  binom  15851  climcndslem1  15870  climcndslem2  15871  cvgrat  15904  clim2prod  15909  prodfn0  15915  prodfrec  15916  ntrivcvgfvn0  15920  prodmolem2a  15955  fprodabs  15995  fprodn0  16000  fprod2d  16002  binomfallfac  16062  bpolycl  16073  bpolydif  16076  fprodefsum  16116  demoivreALT  16224  ruclem8  16260  ruclem9  16261  dvdsle  16335  dvdsfac  16351  divalglem7  16424  bitsinv1  16467  sadcadd  16483  sadadd2  16485  saddisjlem  16489  smuval2  16507  smupvallem  16508  smu01lem  16510  smupval  16513  smueqlem  16515  smumullem  16517  bezoutlem4  16567  dfgcd2  16571  rplpwr  16583  nn0seqcvgd  16595  seq1st  16596  alginv  16600  algcvga  16604  algfx  16605  lcmf  16658  prmind2  16710  prmdvdsexp  16741  prmfac1  16746  reumodprminv  16831  pcmpt  16919  pcfac  16926  prmpwdvds  16931  prmreclem4  16946  vdwlem10  17017  ramval  17035  ramcl  17056  cshwrepswhash1  17129  prmlem1a  17133  imasleval  17562  ismre  17609  mreexexd  17671  lubprop  18379  lublecllem  18381  glbprop  18392  joinlem  18404  meetlem  18418  poslubmo  18432  posglbmo  18433  poslubd  18434  isglbd  18532  lubun  18538  mndind  18853  frmdgsum  18887  mulgnnass  19142  mhmmulg  19148  gsumwrev  19397  gsmsymgrfix  19459  gsmsymgreq  19463  psgnunilem3  19527  sylow1lem1  19629  efginvrel2  19758  efgsrel  19765  efgredlemd  19775  efgredlem  19778  efgred  19779  efgrelexlemb  19781  gsum2dlem2  20002  gsumcom2  20006  ablfac1eulem  20105  pgpfac1lem2  20108  pgpfac1lem5  20112  pgpfac1  20113  pgpfac  20117  isomnd  20154  omndadd  20159  srgmulgass  20254  srgpcomp  20255  srgbinom  20268  isdomn2OLD  20749  isdomn3  20752  isorng  20898  lmodvsmmulgdi  20952  cnfldexp  21445  ofldchr  21616  islindf4  21878  assamulgscm  21941  mplcoe1  22078  mplcoe3  22079  mplcoe5  22081  gsummoncoe1  22359  dmatval  22540  dmatel  22541  dmatmulcl  22548  pmatcoe1fsupp  22749  decpmataa0  22816  decpmatmulsumfsupp  22821  pmatcollpw2lem  22825  pm2mpmhmlem1  22866  fiinopn  22949  mretopd  23140  neiptoptop  23179  cnpfval  23282  iscnp3  23292  tgcn  23300  lmbr  23306  lmbr2  23307  lmbrf  23308  lmss  23346  ishaus  23370  hausnei2  23401  t1sep2  23417  fiuncmp  23452  dfconn2  23467  1stcfb  23493  2ndc1stc  23499  1stcrest  23501  1stcelcls  23509  1stccn  23511  lly1stc  23544  elkgen  23584  kgencn  23604  tx1stc  23698  xkopt  23703  cnmptcom  23726  isr0  23785  r0sep  23796  ptcmpfi  23861  isfildlem  23905  rnelfm  24001  fbflim  24024  flimrest  24031  isflf  24041  flffbas  24043  lmflf  24053  fclsrest  24072  isfcf  24082  cnextfvval  24113  tmdgsum  24143  eltsms  24181  tsmsi  24182  tsmsgsum  24187  tsmssubm  24191  tsmsres  24192  tsmsf1o  24193  isust  24252  isucn  24325  isucn2  24326  ucnima  24328  imasdsf1olem  24421  metss  24556  met1stc  24569  metcnp  24589  metcnpi  24592  metcnpi2  24593  metucn  24619  xrge0tsms  24883  fsumcn  24920  elcncf  24939  cncfi  24944  rescncf  24947  cncfco  24957  caucfil  25333  equivcau  25350  caubl  25358  caublcls  25359  ovolgelb  25530  ovolunlem1a  25546  ovolicc2lem3  25569  voliunlem1  25600  voliunlem3  25602  volsuplem  25605  volsup  25606  dyadmax  25648  vitali  25663  itg2leub  25784  itgfsum  25877  dvnadd  25979  dvnres  25981  cpnord  25985  dvnfre  26002  dvmptfsum  26025  dvferm1  26035  dvferm2  26037  rolle  26040  dvlip  26043  c1lip1  26047  lhop1  26064  deg1leb  26143  ply1divex  26185  fta1g  26218  plyco  26289  dgrcolem1  26321  dgrco  26323  dvnply2  26339  plydivex  26349  aalioulem2  26385  aalioulem3  26386  aalioulem5  26388  aaliou3lem2  26395  dvntaylp  26422  taylthlem1  26424  ulmdvlem3  26453  abelthlem9  26491  cxpmul2  26742  scvxcvx  27038  jensenlem2  27040  jensen  27041  wilthlem3  27122  perfectlem2  27282  bcmono  27329  bposlem5  27340  lgsquad2lem2  27437  addsq2reu  27492  2sqreulem1  27498  2sqreunnlem1  27501  dchrisumlem1  27541  dchrisum0flb  27562  pntpbnd1  27638  pntlemf  27657  qabvle  27677  qabvexp  27678  ostthlem2  27680  ostth2lem2  27686  nosupcbv  27754  nosupno  27755  nosupdm  27756  nosupfv  27758  nosupres  27759  nosupbnd1lem1  27760  nosupbnd1lem3  27762  nosupbnd1lem5  27764  noinfcbv  27769  noinfno  27770  noinfdm  27771  noinffv  27773  noinfres  27774  noinfbnd1lem3  27777  noinfbnd1lem5  27779  eqcuts2  27867  addsproplem1  28050  addsprop  28057  negsunif  28136  mulsproplem9  28205  sltmuls2  28229  precsexlem8  28295  precsexlem9  28296  precsexlem11  28298  noseqind  28373  om2noseqrdg  28385  noseqrdgfn  28387  n0addscl  28425  n0mulscl  28426  eucliddivs  28457  peano5uzs  28485  expscllem  28511  expadds  28516  expsne0  28517  expsgt0  28518  pw2cut  28541  pw2cut2  28543  bdaypw2n0bnd  28545  tgcgr4  28688  usgr2pth  29921  wlkiswwlks2lem4  30029  wlkiswwlks2  30032  rusgrnumwwlk  30135  clwlkclwwlklem2a  30157  clwlkclwwlklem1  30158  clwlkclwwlkfo  30168  eupth2  30398  frgr3vlem1  30432  3vfriswmgrlem  30436  3vfriswmgr  30437  wlkl0  30526  numclwlk2lem2f1o  30538  isplig  30636  isnvlem  30770  nvi  30774  nmoubi  30932  nmounbi  30936  nmblolbi  30960  ipasslem1  30991  ipassi  31001  hlim2  31352  pjhth  31553  spansni  31717  elspansn2  31727  pjige0  31851  pjcjt2  31852  pjopyth  31880  elcnop  32017  elcnfn  32042  nmopub  32068  cnopc  32073  nmfnleub  32085  elnlfn  32088  cnfnc  32090  nmbdoplb  32185  nmcexi  32186  nmcoplb  32190  lnfnmul  32208  nmbdfnlb  32210  nmcfnlb  32214  pjss2coi  32324  pjssmi  32325  isst  32373  ishst  32374  stcltr1i  32434  mdbr  32454  dmdbr  32459  mddmd2  32469  mdslmd1lem3  32487  mdslmd1lem4  32488  elat2  32500  atcvat2  32549  cdj1i  32593  iuninc  32720  fmptcof2  32820  nn0min  32984  nexple  32996  wrdt2ind  33092  ismnt  33122  xrge0tsmsd  33214  gsumwun  33217  cyc3genpm  33293  isarchi2  33326  archirng  33329  archiexdiv  33331  archiabl  33339  domnprodn0  33420  islbs5  33527  unitprodclb  33536  mxidlval  33610  1arithidom  33694  1arithufdlem3  33703  crefeq  34103  esumfzf  34327  issiga  34370  isrnsiga  34371  isldsys  34414  ismeas  34457  isrnmeas  34458  measiun  34476  eulerpartlemn  34639  sseqp1  34653  rrvsum  34712  signsply0  34806  signstfvc  34829  bnj941  35029  bnj106  35124  bnj155  35135  bnj590  35166  bnj591  35167  bnj849  35181  bnj893  35184  bnj944  35194  bnj1128  35246  r1filimi  35360  r1omhfb  35369  tz9.1regs  35391  r1omhfbregs  35394  gblacfnacd  35406  subfacp1lem6  35496  erdszelem8  35509  issconn  35537  cvmliftlem7  35602  cvmliftlem10  35605  cvmlift3lem2  35631  satfsschain  35675  satfrel  35678  satfdm  35680  satfrnmapom  35681  fmlafvel  35696  satffun  35720  mrsubvrs  35833  mclsssvlem  35873  mclsval  35874  mclsax  35880  mclsind  35881  shftvalg  36043  bccolsum  36050  iprodefisumlem  36051  faclimlem1  36054  rdgprc  36103  sbequbidv  36535  cbvsbdavw  36575  fveleq  36772  dfttc4lem1  36849  dfttc4  36851  elttcirr  36852  regsfromregtco  36859  mh-unprimbi  36865  unblimceq0  36906  bj-ax12  37090  bj-bm1.3ii  37510  rdgeqoa  37825  finxpreclem6  37851  domalom  37859  ralssiun  37862  wl-ax12v2cl  37961  wl-sblimt  38012  wl-sbhbt  38018  wl-2sb6d  38022  wl-mo2df  38034  wl-mo2t  38039  poimirlem2  38082  poimirlem25  38105  poimirlem28  38108  poimirlem31  38111  heicant  38115  mbfresfi  38126  itg2gt0cn  38135  sdclem2  38202  fdc  38205  seqpo  38207  incsequz  38208  mettrifi  38217  prdsbnd2  38255  heiborlem4  38274  bfplem1  38282  iscringd  38458  maxidlval  38499  igenval2  38526  iss2  38804  elrefrels3  39059  ax12eq  39526  ax12el  39527  ax12indalem  39530  ax12inda2ALT  39531  ax12inda  39533  ax12v2-o  39534  riotasvd  39541  isopos  39765  isat3  39892  ishlat1  39937  glbconN  39962  ispsubsp  40330  isldil  40695  isltrn  40704  isdilN  40739  trlval  40747  cdleme27b  40953  cdleme29b  40960  cdleme31sn1  40966  cdleme31sn1c  40973  cdleme40v  41054  cdlemk36  41498  cdlemkid5  41520  cdlemn11pre  41795  dihord2pre  41810  islpolN  42068  hdmapffval  42411  hdmapfval  42412  hdmapval2lem  42416  uzindd  42556  sticksstones1  42724  sticksstones2  42725  sticksstones3  42726  sticksstones8  42731  sticksstones10  42733  sticksstones11  42734  sticksstones12a  42735  sticksstones15  42739  indstrd  42771  unitscyglem3  42775  eu6w  43219  ismrc  43243  incssnn0  43253  mzpexpmpt  43287  pell14qrexpclnn0  43404  monotuz  43479  rmxypos  43485  jm2.17a  43498  jm2.17b  43499  rmygeid  43502  jm2.18  43526  jm2.19lem3  43529  jm2.25  43537  jm2.15nn0  43541  jm2.16nn0  43542  wepwsolem  43580  aomclem8  43599  dfac11  43600  pwslnm  43632  lnr2i  43654  hbtlem5  43666  cnsrexpcl  43703  rngunsnply  43707  unielss  43756  onsucf1lem  43807  cantnfresb  43862  onmcl  43869  naddonnn  43933  elmapintrab  44113  elmapintab  44133  cnvcnvintabd  44137  eliunov2  44216  relexpxpnnidm  44240  relexpiidm  44241  relexpss1d  44242  iunrelexpmin1  44245  relexpmulnn  44246  iunrelexpmin2  44249  relexp0a  44253  trclimalb2  44263  clsk3nimkb  44577  ntrclsiso  44604  ntrclskb  44606  ntrneiiso  44628  ntrneix2  44630  ntrneixb  44632  gneispace2  44669  gneispacess2  44683  mnuunid  44814  dvgrat  44849  pm14.122b  44960  relpeq1  45481  relpeq3  45483  trfr  45499  pwclaxpow  45521  prclaxpr  45522  uniclaxun  45523  modelac8prim  45529  permaxpow  45546  permaxpr  45547  permaxun  45548  nregmodel  45554  fnchoice  45570  fiiuncl  45606  ssinc  45626  ssdec  45627  wessf1ornlem  45724  dmrelrnrel  45763  fperiodmullem  45843  monoordxrv  46016  fmul01  46117  fmuldfeq  46120  climsuselem1  46144  climinff  46148  ellimcabssub0  46154  limcleqr  46179  addlimc  46183  0ellimcdiv  46184  limclner  46186  limsupref  46220  limsupub  46239  limsupmnf  46256  limsupre2lem  46259  limsupre2  46260  limsupre2mpt  46265  limsupre3lem  46267  limsupre3  46268  limsupre3mpt  46269  xlimbr  46362  cnrefiisplem  46364  dvnmptdivc  46473  dvnmptconst  46476  dvnmul  46478  iblspltprt  46508  itgspltprt  46514  stoweidlem2  46537  stoweidlem3  46538  stoweidlem17  46552  stoweidlem19  46554  stoweidlem21  46556  stoweidlem26  46561  fourierdlem42  46684  issal  46849  ismea  46986  isome  47029  carageniuncllem1  47056  caratheodorylem1  47061  2reu8i  47668  2reuimp0  47669  funressndmafv2rn  47778  2ffzoeq  47883  smonoord  47932  fargshiftf1  48008  ichnfimlem  48030  paireqne  48078  reupr  48089  reuopreuprim  48093  perfectALTVlem2  48305  grimcnv  48471  pgnbgreunbgrlem1  48696  pgnbgreunbgrlem4  48702  pgnbgreunbgr  48708  lmodvsmdi  48962  dmatALTval  48983  dmatALTbasel  48985  snlindsntor  49054  ldepsnlinc  49091  elbigo2r  49136  elbigolo1  49140  itcovalt2  49260  mof0  49420  isnrm4  49513  iscnrm3r  49530  iscnrm4  49536  lubsscl  49542  glbsscl  49543  ipolubdm  49569  ipoglbdm  49572  setrecseq  50267  setrec2fun  50274  setrec2lem2  50276