Theorem imbi2d 343

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 26	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒)))
3	2	pm5.74d 276	1 ⊢ (𝜑 → ((𝜃 → 𝜓) ↔ (𝜃 → 𝜒)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  imbi12d  347  imbi2  351  pm5.42  553  orbi2d  929  19.23t  2249  axc14  2497  mojust  2568  mof  2593  eu6lem  2603  2gencl  3499  3gencl  3500  vtocl2gf  3538  vtocl3gf  3539  vtocl2g  3540  vtocl3g  3541  vtocl2ga  3544  vtocl2gaf  3545  vtocl3gaf  3546  vtocl3ga  3547  vtocl4g  3548  vtocl4ga  3549  eqeu  3671  mo2icl  3679  euind  3689  reu7  3697  reuind  3718  sbctt  3815  sbccomlem  3824  reu8nf  3831  sbcnestgfw  4386  sbcnestgf  4391  r19.36zv  4475  dedth2h  4549  dedth3h  4550  dedth4h  4551  reusngf  4642  reuprg0  4670  preq12bg  4820  elint  4920  elintrabg  4928  intab  4945  axrep1  5241  axreplem  5242  axrep2  5243  axrep6g  5253  bm1.3iiOLD  5267  reusv3  5378  swopolem  5581  solin  5598  freq1  5630  frminex  5642  vtoclr  5726  2optocl  5759  3optocl  5760  raliunxp  5827  resieq  5991  iss  6039  cnveqb  6197  reu3op  6297  reuop  6298  dfpo2  6301  preddowncl  6337  fnbrfvb  6935  fvelimab  6957  fvmptss  7006  fmptco  7129  fprg  7156  fnressn  7159  fressnfv  7161  isoselem  7345  ovg  7581  caovcan  7620  caovordig  7621  caovord  7627  tfisi  7857  tfindsg  7859  tfinds2  7862  tfinds3  7863  dfom2  7866  elom  7867  findsg  7896  finds2  7897  resf1extb  7933  f1o2ndf1  8119  poxp  8126  fnse  8131  xpord3inddlem  8152  soseq  8157  fpr3g  8284  frrlem12  8296  fpr2a  8301  wfr3g  8318  smoeq  8339  smores  8341  smogt  8356  tfrlem1  8364  tfr3  8388  oaordi  8533  oeordi  8575  oeoa  8585  oeoe  8587  nnacl  8599  nnmcl  8600  nnecl  8601  nnacom  8605  nnaordi  8606  nnawordi  8609  nnaass  8610  nndi  8611  nnmass  8612  nnmsucr  8613  nnmcom  8614  nnmordi  8619  naddssim  8674  naddoa  8691  2ecoptocl  8808  3ecoptocl  8809  undifixp  8934  xpdom2g  9064  findcard2  9152  unfi  9158  ssfi  9160  fnfi  9165  fodomfi  9275  finsschain  9319  marypha1lem  9396  marypha1  9397  supeq1  9408  ordiso2  9480  ordtypelem7  9489  wemaplem1  9511  inf3lem2  9601  inf3lem5  9604  infdiffi  9630  cantnfval2  9641  cantnfle  9643  cantnfp1lem3  9652  oemapval  9655  cantnflem1  9661  cantnf  9665  wemapwe  9669  cnfcom  9672  cnfcom3clem  9677  ttrclss  9692  ttrclselem2  9698  tz9.1  9701  frr3g  9731  frr2  9735  r1pwALT  9821  cplem2  9884  cplem2OLD  9885  kardenOLD  9892  updjud  9932  infxpenc2lem2  10016  fseqenlem1  10020  dfac8clem  10028  alephinit  10091  dfac4  10118  dfac5lem5  10123  dfac2a  10125  dfac2b  10126  dfacacn  10137  dfac12lem3  10141  kmlem2  10147  kmlem13  10158  nnadju  10193  ackbij1lem16  10229  sornom  10272  infpssrlem4  10301  fin23lem14  10328  fin23lem32  10339  fin23lem34  10341  fin23lem36  10343  isf32lem1  10348  isf32lem2  10349  axcc2lem  10431  axcc3  10433  axcclem  10452  zornn0g  10500  ttukeylem5  10508  ttukeylem6  10509  axrepnd  10590  axpowndlem3  10595  zfcndrep  10610  fpwwe2lem7  10633  pwfseqlem3  10656  wunr1om  10715  wunfi  10717  tskr1om  10763  ingru  10811  grudomon  10813  axgroth3  10827  axgroth4  10828  nqereu  10925  mulcanenq  10956  elnp  10983  elnpi  10984  prlem934  11029  infm3  12185  nnindd  12264  nnaddcl  12267  nnmulcl  12268  nnaddcom  12271  nnne0  12281  nnadddir  12303  nnmulcom  12305  peano5uzi  12697  uzind2  12701  nn0indd  12705  zindd  12709  fzindd  12710  uzaddcl  12940  uzwo  12947  indstr  12952  zmax  12981  xmulasslem  13323  xrsupsslem  13345  xrinfmsslem  13346  xrsupss  13347  xrinfmss  13348  flval2  13861  om2uzlti  14000  uzrdgfni  14008  rabssnn0fi  14036  mptnn0fsupp  14047  seqcl2  14070  seqfveq2  14074  seqshft2  14078  monoord  14082  seqsplit  14085  seqcaopr3  14087  seqf1olem2a  14090  seqf1o  14093  seqid2  14098  seqhomo  14099  ser1const  14108  expcllem  14122  expeq0  14142  mulexp  14151  expadd  14154  expmul  14157  expmordi  14217  leexp2r  14224  leexp1a  14225  bernneq  14279  modexp  14288  facdiv  14337  faclbnd  14340  faclbnd4lem4  14346  hashgadd  14427  hashxp  14485  hashmap  14486  hashf1lem2  14507  hashf1  14508  seqcoll  14515  wrdind  14777  wrd2ind  14778  pfxccatin12lem3  14787  cshweqrep  14878  2cshwcshw  14882  relexp0g  15079  relexpsucnnr  15082  relexpsucnnl  15087  relexpcnv  15092  relexpnndm  15098  relexpaddnn  15108  rtrclreclem1  15114  dfrtrclrec2  15115  rtrclreclem2  15116  rtrclreclem4  15118  dfrtrcl2  15119  relexpind  15121  reusq0  15536  rlim  15566  rlim2  15567  rlim0  15579  rlim0lt  15580  rlimi  15584  ello12r  15588  ello1mpt  15592  ello1d  15594  elo12r  15599  lo1o1  15603  o1lo1  15608  lo1res  15630  climshft  15647  o1compt  15658  rlimo1  15688  lo1add  15698  lo1mul  15699  rlimdiv  15717  climub  15733  climserle  15734  caucvgrlem  15744  caurcvgr  15745  iseraltlem2  15754  summolem2a  15785  sumss  15794  fsum2d  15841  fsumabs  15872  fsumrlim  15882  fsumo1  15883  fsumiun  15892  binom  15903  climcndslem1  15922  climcndslem2  15923  cvgrat  15956  clim2prod  15961  prodfn0  15967  prodfrec  15968  ntrivcvgfvn0  15972  prodmolem2a  16007  fprodabs  16047  fprodn0  16052  fprod2d  16054  binomfallfac  16113  bpolycl  16124  bpolydif  16127  fprodefsum  16167  demoivreALT  16275  ruclem8  16311  ruclem9  16312  dvdsle  16386  dvdsfac  16402  divalglem7  16475  bitsinv1  16518  sadcadd  16534  sadadd2  16536  saddisjlem  16540  smuval2  16558  smupvallem  16559  smu01lem  16561  smupval  16564  smueqlem  16566  smumullem  16568  bezoutlem4  16618  dfgcd2  16622  rplpwr  16634  nn0seqcvgd  16646  seq1st  16647  alginv  16651  algcvga  16655  algfx  16656  lcmf  16709  prmind2  16761  prmdvdsexp  16792  prmfac1  16797  reumodprminv  16882  pcmpt  16970  pcfac  16977  prmpwdvds  16982  prmreclem4  16997  vdwlem10  17068  ramval  17086  ramcl  17107  cshwrepswhash1  17180  prmlem1a  17184  imasleval  17613  ismre  17660  mreexexd  17722  lubprop  18430  lublecllem  18432  glbprop  18443  joinlem  18455  meetlem  18469  poslubmo  18483  posglbmo  18484  poslubd  18485  isglbd  18583  lubun  18589  mndind  18911  frmdgsum  18945  mulgnnass  19199  mhmmulg  19205  gsumwrev  19460  gsmsymgrfix  19522  gsmsymgreq  19526  psgnunilem3  19590  sylow1lem1  19692  efginvrel2  19821  efgsrel  19828  efgredlemd  19838  efgredlem  19841  efgred  19842  efgrelexlemb  19844  gsum2dlem2  20065  gsumcom2  20069  ablfac1eulem  20168  pgpfac1lem2  20171  pgpfac1lem5  20175  pgpfac1  20176  pgpfac  20180  isomnd  20217  omndadd  20222  srgmulgass  20323  srgpcomp  20324  srgbinom  20337  isdomn3  20843  isorng  20994  lmodvsmmulgdi  21048  rspprop  21400  cnfldexp  21585  ofldchr  21756  islindf4  22018  assamulgscm  22081  mplcoe1  22218  mplcoe3  22219  mplcoe5  22221  gsummoncoe1  22498  dmatval  22679  dmatel  22680  dmatmulcl  22687  pmatcoe1fsupp  22888  decpmataa0  22955  decpmatmulsumfsupp  22960  pmatcollpw2lem  22964  pm2mpmhmlem1  23005  fiinopn  23088  mretopd  23279  neiptoptop  23318  cnpfval  23421  iscnp3  23431  tgcn  23439  lmbr  23445  lmbr2  23446  lmbrf  23447  lmss  23485  ishaus  23509  hausnei2  23540  t1sep2  23556  fiuncmp  23591  dfconn2  23606  1stcfb  23632  2ndc1stc  23638  1stcrest  23640  1stcelcls  23649  1stccn  23651  lly1stc  23684  elkgen  23724  kgencn  23744  tx1stc  23838  xkopt  23843  cnmptcom  23866  isr0  23925  r0sep  23936  ptcmpfi  24001  isfildlem  24045  rnelfm  24141  fbflim  24164  flimrest  24171  isflf  24181  flffbas  24183  lmflf  24193  fclsrest  24212  isfcf  24222  cnextfvval  24253  tmdgsum  24283  eltsms  24321  tsmsi  24322  tsmsgsum  24327  tsmssubm  24331  tsmsres  24332  tsmsf1o  24333  isust  24392  isucn  24465  isucn2  24466  ucnima  24468  imasdsf1olem  24561  metss  24696  met1stc  24709  metcnp  24729  metcnpi  24732  metcnpi2  24733  metucn  24759  xrge0tsms  25023  fsumcn  25060  elcncf  25079  cncfi  25084  rescncf  25087  cncfco  25097  caucfil  25473  equivcau  25490  caubl  25498  caublcls  25499  ovolgelb  25670  ovolunlem1a  25686  ovolicc2lem3  25709  voliunlem1  25740  voliunlem3  25742  volsuplem  25745  volsup  25746  dyadmax  25788  vitali  25803  itg2leub  25924  itgfsum  26017  dvnadd  26119  dvnres  26121  cpnord  26125  dvnfre  26142  dvmptfsum  26165  dvferm1  26175  dvferm2  26177  rolle  26180  dvlip  26183  c1lip1  26187  lhop1  26204  deg1leb  26283  ply1divex  26325  fta1g  26358  plyco  26429  dgrcolem1  26461  dgrco  26463  dvnply2  26479  plydivex  26489  aalioulem2  26527  aalioulem3  26528  aalioulem5  26530  aaliou3lem2  26537  dvntaylp  26565  taylthlem1  26567  ulmdvlem3  26596  abelthlem9  26634  cxpmul2  26885  scvxcvx  27181  jensenlem2  27183  jensen  27184  wilthlem3  27265  perfectlem2  27425  bcmono  27472  bposlem5  27483  lgsquad2lem2  27580  addsq2reu  27635  2sqreulem1  27641  2sqreunnlem1  27644  dchrisumlem1  27684  dchrisum0flb  27705  pntpbnd1  27781  pntlemf  27800  qabvle  27820  qabvexp  27821  ostthlem2  27823  ostth2lem2  27829  nosupcbv  27897  nosupno  27898  nosupdm  27899  nosupfv  27901  nosupres  27902  nosupbnd1lem1  27903  nosupbnd1lem3  27905  nosupbnd1lem5  27907  noinfcbv  27912  noinfno  27913  noinfdm  27914  noinffv  27916  noinfres  27917  noinfbnd1lem3  27920  noinfbnd1lem5  27922  eqcuts2  28010  addsproplem1  28193  addsprop  28200  negsunif  28279  mulsproplem9  28348  sltmuls2  28372  precsexlem8  28438  precsexlem9  28439  precsexlem11  28441  noseqind  28516  om2noseqrdg  28528  noseqrdgfn  28530  n0addscl  28568  n0mulscl  28569  eucliddivs  28600  peano5uzs  28628  expscllem  28654  expadds  28659  expsne0  28660  expsgt0  28661  pw2cut  28684  pw2cut2  28686  bdaypw2n0bnd  28688  tgcgr4  28831  prlngmo2  29237  usgr2pth  30153  wlkiswwlks2lem4  30264  wlkiswwlks2  30267  rusgrnumwwlk  30370  clwlkclwwlklem2a  30392  clwlkclwwlklem1  30393  clwlkclwwlkfo  30403  eupth2  30637  frgr3vlem1  30671  3vfriswmgrlem  30675  3vfriswmgr  30676  wlkl0  30765  numclwlk2lem2f1o  30777  isplig  30875  isnvlem  31009  nvi  31013  nmoubi  31171  nmounbi  31175  nmblolbi  31199  ipasslem1  31230  ipassi  31240  hlim2  31591  pjhth  31792  spansni  31956  elspansn2  31966  pjige0  32090  pjcjt2  32091  pjopyth  32119  elcnop  32256  elcnfn  32281  nmopub  32307  cnopc  32312  nmfnleub  32324  elnlfn  32327  cnfnc  32329  nmbdoplb  32424  nmcexi  32425  nmcoplb  32429  lnfnmul  32447  nmbdfnlb  32449  nmcfnlb  32453  pjss2coi  32563  pjssmi  32564  isst  32612  ishst  32613  stcltr1i  32673  mdbr  32693  dmdbr  32698  mddmd2  32708  mdslmd1lem3  32726  mdslmd1lem4  32727  elat2  32739  atcvat2  32788  cdj1i  32832  iuninc  32952  fmptcof2  33049  nn0min  33211  nexple  33223  wrdt2ind  33315  ismnt  33343  xrge0tsmsd  33433  gsumwun  33436  cyc3genpm  33512  isarchi2  33545  archirng  33548  archiexdiv  33550  archiabl  33558  domnprodn0  33638  islbs5  33733  unitprodclb  33742  mxidlval  33784  1arithidom  33867  1arithufdlem3  33876  crefeq  34275  esumfzf  34499  issiga  34542  isrnsiga  34543  isldsys  34587  ismeas  34630  isrnmeas  34631  measiun  34649  eulerpartlemn  34812  sseqp1  34826  rrvsum  34885  signsply0  34979  signstfvc  35002  bnj941  35202  bnj106  35297  bnj155  35308  bnj590  35339  bnj591  35340  bnj849  35354  bnj893  35357  bnj944  35367  bnj1128  35419  r1filimi  35531  r1omhfb  35542  tz9.1regs  35580  r1omhfbregs  35583  elkarden  35601  gblacfnacd  35619  subfacp1lem6  35690  erdszelem8  35703  issconn  35731  cvmliftlem7  35796  cvmliftlem10  35799  cvmlift3lem2  35825  satfsschain  35869  satfrel  35872  satfdm  35874  satfrnmapom  35875  fmlafvel  35890  satffun  35914  mrsubvrs  36027  mclsssvlem  36067  mclsval  36068  mclsax  36074  mclsind  36075  shftvalg  36237  bccolsum  36244  iprodefisumlem  36245  faclimlem1  36248  rdgprc  36297  nmuladdss  36718  sbequbidv  36759  cbvsbdavw  36799  fveleq  36995  dfttc4lem1  37072  dfttc4  37074  elttcirr  37075  regsfromregtco  37082  mh-unprimbi  37088  unblimceq0  37129  bj-ax12  37312  bj-bm1.3ii  37733  rdgeqoa  38049  finxpreclem6  38075  domalom  38083  ralssiun  38086  wl-ax12v2cl  38185  wl-sblimt  38236  wl-sbhbt  38242  wl-2sb6d  38246  wl-mo2df  38258  wl-mo2t  38263  poimirlem2  38306  poimirlem25  38329  poimirlem28  38332  poimirlem31  38335  heicant  38339  mbfresfi  38350  itg2gt0cn  38359  sdclem2  38426  fdc  38429  seqpo  38431  incsequz  38432  mettrifi  38441  prdsbnd2  38479  heiborlem4  38498  bfplem1  38506  iscringd  38682  maxidlval  38723  igenval2  38750  iss2  39026  elrefrels3  39281  ax12eq  39748  ax12el  39749  ax12indalem  39752  ax12inda2ALT  39753  ax12inda  39755  ax12v2-o  39756  riotasvd  39763  isopos  39987  isat3  40114  ishlat1  40159  glbconN  40184  ispsubsp  40552  isldil  40917  isltrn  40926  isdilN  40961  trlval  40969  cdleme27b  41175  cdleme29b  41182  cdleme31sn1  41188  cdleme31sn1c  41195  cdleme40v  41276  cdlemk36  41720  cdlemkid5  41742  cdlemn11pre  42017  dihord2pre  42032  islpolN  42290  hdmapffval  42633  hdmapfval  42634  hdmapval2lem  42638  uzindd  42778  sticksstones1  42946  sticksstones2  42947  sticksstones3  42948  sticksstones8  42953  sticksstones10  42955  sticksstones11  42956  sticksstones12a  42957  sticksstones15  42961  indstrd  42993  unitscyglem3  42997  eu6w  43441  ismrc  43465  incssnn0  43475  mzpexpmpt  43509  pell14qrexpclnn0  43626  monotuz  43701  rmxypos  43707  jm2.17a  43720  jm2.17b  43721  rmygeid  43724  jm2.18  43748  jm2.19lem3  43751  jm2.25  43759  jm2.15nn0  43763  jm2.16nn0  43764  wepwsolem  43802  aomclem8  43821  dfac11  43822  pwslnm  43854  lnr2i  43876  hbtlem5  43888  cnsrexpcl  43925  rngunsnply  43929  unielss  43978  onsucf1lem  44029  cantnfresb  44084  onmcl  44091  naddonnn  44155  elmapintrab  44335  elmapintab  44355  cnvcnvintabd  44359  eliunov2  44438  relexpxpnnidm  44462  relexpiidm  44463  relexpss1d  44464  iunrelexpmin1  44467  relexpmulnn  44468  iunrelexpmin2  44471  relexp0a  44475  trclimalb2  44485  clsk3nimkb  44799  ntrclsiso  44826  ntrclskb  44828  ntrneiiso  44850  ntrneix2  44852  ntrneixb  44854  gneispace2  44891  gneispacess2  44905  mnuunid  45020  dvgrat  45055  pm14.122b  45166  relpeq1  45686  relpeq3  45688  trfr  45704  pwclaxpow  45726  prclaxpr  45727  uniclaxun  45728  modelac8prim  45734  permaxpow  45751  permaxpr  45752  permaxun  45753  nregmodel  45759  fnchoice  45782  fiiuncl  45818  ssinc  45838  ssdec  45839  wessf1ornlem  45936  dmrelrnrel  45975  fperiodmullem  46055  monoordxrv  46228  fmul01  46329  fmuldfeq  46332  climsuselem1  46356  climinff  46360  ellimcabssub0  46366  limcleqr  46391  addlimc  46395  0ellimcdiv  46396  limclner  46398  limsupref  46432  limsupub  46451  limsupmnf  46468  limsupre2lem  46471  limsupre2  46472  limsupre2mpt  46477  limsupre3lem  46479  limsupre3  46480  limsupre3mpt  46481  xlimbr  46574  cnrefiisplem  46576  dvnmptdivc  46685  dvnmptconst  46688  dvnmul  46690  iblspltprt  46720  itgspltprt  46726  stoweidlem2  46749  stoweidlem3  46750  stoweidlem17  46764  stoweidlem19  46766  stoweidlem21  46768  stoweidlem26  46773  fourierdlem42  46896  issal  47061  ismea  47198  isome  47241  carageniuncllem1  47268  caratheodorylem1  47273  2reu8i  47883  2reuimp0  47884  funressndmafv2rn  47993  2ffzoeq  48098  smonoord  48147  fargshiftf1  48223  ichnfimlem  48245  paireqne  48293  reupr  48304  reuopreuprim  48308  perfectALTVlem2  48520  grimcnv  48686  pgnbgreunbgrlem1  48911  pgnbgreunbgrlem4  48917  pgnbgreunbgr  48923  lmodvsmdi  49192  dmatALTval  49213  dmatALTbasel  49215  snlindsntor  49284  ldepsnlinc  49321  elbigo2r  49366  elbigolo1  49370  itcovalt2  49490  mof0  49649  isnrm4  49742  iscnrm3r  49759  iscnrm4  49765  lubsscl  49771  glbsscl  49772  ipolubdm  49798  ipoglbdm  49801  setrecseq  50496  setrec2fun  50503  setrec2lem2  50505