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  552  orbi2d  928  19.23t  2246  axc14  2495  mojust  2566  mof  2591  eu6lem  2601  2gencl  3497  3gencl  3498  vtocl2gf  3536  vtocl3gf  3537  vtocl2g  3538  vtocl3g  3539  vtocl2ga  3542  vtocl2gaf  3543  vtocl3gaf  3544  vtocl3ga  3545  vtocl4g  3546  vtocl4ga  3547  eqeu  3669  mo2icl  3677  euind  3687  reu7  3695  reuind  3716  sbctt  3813  sbccomlem  3822  reu8nf  3830  sbcnestgfw  4386  sbcnestgf  4391  r19.36zv  4473  dedth2h  4547  dedth3h  4548  dedth4h  4549  reusngf  4640  reuprg0  4668  preq12bg  4818  elint  4918  elintrabg  4926  intab  4943  axrep1  5239  axreplem  5240  axrep2  5241  axrep6g  5251  bm1.3iiOLD  5265  reusv3  5376  swopolem  5579  solin  5596  freq1  5628  frminex  5640  vtoclr  5724  2optocl  5757  3optocl  5758  raliunxp  5825  resieq  5989  iss  6037  cnveqb  6195  reu3op  6293  reuop  6294  dfpo2  6297  preddowncl  6333  fnbrfvb  6931  fvelimab  6953  fvmptss  7002  fmptco  7125  fprg  7152  fnressn  7155  fressnfv  7157  isoselem  7339  ovg  7575  caovcan  7614  caovordig  7615  caovord  7621  tfisi  7851  tfindsg  7853  tfinds2  7856  tfinds3  7857  dfom2  7860  elom  7861  findsg  7890  finds2  7891  resf1extb  7927  f1o2ndf1  8113  poxp  8120  fnse  8125  xpord3inddlem  8146  soseq  8151  fpr3g  8278  frrlem12  8290  fpr2a  8295  wfr3g  8312  smoeq  8333  smores  8335  smogt  8350  tfrlem1  8358  tfr3  8382  oaordi  8527  oeordi  8569  oeoa  8579  oeoe  8581  nnacl  8593  nnmcl  8594  nnecl  8595  nnacom  8599  nnaordi  8600  nnawordi  8603  nnaass  8604  nndi  8605  nnmass  8606  nnmsucr  8607  nnmcom  8608  nnmordi  8613  naddssim  8668  naddoa  8685  2ecoptocl  8802  3ecoptocl  8803  undifixp  8928  xpdom2g  9057  findcard2  9145  unfi  9151  ssfi  9153  fnfi  9158  fodomfi  9268  finsschain  9312  marypha1lem  9389  marypha1  9390  supeq1  9401  ordiso2  9473  ordtypelem7  9482  wemaplem1  9504  inf3lem2  9594  inf3lem5  9597  infdiffi  9623  cantnfval2  9634  cantnfle  9636  cantnfp1lem3  9645  oemapval  9648  cantnflem1  9654  cantnf  9658  wemapwe  9662  cnfcom  9665  cnfcom3clem  9670  ttrclss  9685  ttrclselem2  9691  tz9.1  9694  frr3g  9724  frr2  9728  r1pwALT  9814  cplem2  9877  cplem2OLD  9878  kardenOLD  9885  updjud  9925  infxpenc2lem2  10009  fseqenlem1  10013  dfac8clem  10021  alephinit  10084  dfac4  10111  dfac5lem5  10116  dfac2a  10118  dfac2b  10119  dfacacn  10130  dfac12lem3  10134  kmlem2  10140  kmlem13  10151  nnadju  10186  ackbij1lem16  10222  sornom  10265  infpssrlem4  10294  fin23lem14  10321  fin23lem32  10332  fin23lem34  10334  fin23lem36  10336  isf32lem1  10341  isf32lem2  10342  axcc2lem  10424  axcc3  10426  axcclem  10445  zornn0g  10493  ttukeylem5  10501  ttukeylem6  10502  axrepnd  10583  axpowndlem3  10588  zfcndrep  10603  fpwwe2lem7  10626  pwfseqlem3  10649  wunr1om  10708  wunfi  10710  tskr1om  10756  ingru  10804  grudomon  10806  axgroth3  10820  axgroth4  10821  nqereu  10918  mulcanenq  10949  elnp  10976  elnpi  10977  prlem934  11022  infm3  12178  nnindd  12257  nnaddcl  12260  nnmulcl  12261  nnaddcom  12264  nnne0  12274  nnadddir  12296  nnmulcom  12298  peano5uzi  12689  uzind2  12693  nn0indd  12697  zindd  12701  fzindd  12702  uzaddcl  12932  uzwo  12939  indstr  12944  zmax  12973  xmulasslem  13315  xrsupsslem  13337  xrinfmsslem  13338  xrsupss  13339  xrinfmss  13340  flval2  13852  om2uzlti  13991  uzrdgfni  13999  rabssnn0fi  14027  mptnn0fsupp  14038  seqcl2  14061  seqfveq2  14065  seqshft2  14069  monoord  14073  seqsplit  14076  seqcaopr3  14078  seqf1olem2a  14081  seqf1o  14084  seqid2  14089  seqhomo  14090  ser1const  14099  expcllem  14113  expeq0  14133  mulexp  14142  expadd  14145  expmul  14148  expmordi  14208  leexp2r  14215  leexp1a  14216  bernneq  14270  modexp  14279  facdiv  14328  faclbnd  14331  faclbnd4lem4  14337  hashgadd  14418  hashxp  14476  hashmap  14477  hashf1lem2  14498  hashf1  14499  seqcoll  14506  wrdind  14764  wrd2ind  14765  pfxccatin12lem3  14774  cshweqrep  14863  2cshwcshw  14867  relexp0g  15064  relexpsucnnr  15067  relexpsucnnl  15072  relexpcnv  15077  relexpnndm  15083  relexpaddnn  15093  rtrclreclem1  15099  dfrtrclrec2  15100  rtrclreclem2  15101  rtrclreclem4  15103  dfrtrcl2  15104  relexpind  15106  reusq0  15521  rlim  15551  rlim2  15552  rlim0  15564  rlim0lt  15565  rlimi  15569  ello12r  15573  ello1mpt  15577  ello1d  15579  elo12r  15584  lo1o1  15588  o1lo1  15593  lo1res  15615  climshft  15632  o1compt  15643  rlimo1  15673  lo1add  15683  lo1mul  15684  rlimdiv  15702  climub  15718  climserle  15719  caucvgrlem  15729  caurcvgr  15730  iseraltlem2  15739  summolem2a  15771  sumss  15780  fsum2d  15827  fsumabs  15858  fsumrlim  15868  fsumo1  15869  fsumiun  15878  binom  15889  climcndslem1  15908  climcndslem2  15909  cvgrat  15942  clim2prod  15947  prodfn0  15953  prodfrec  15954  ntrivcvgfvn0  15958  prodmolem2a  15993  fprodabs  16033  fprodn0  16038  fprod2d  16040  binomfallfac  16099  bpolycl  16110  bpolydif  16113  fprodefsum  16153  demoivreALT  16261  ruclem8  16297  ruclem9  16298  dvdsle  16372  dvdsfac  16388  divalglem7  16461  bitsinv1  16504  sadcadd  16520  sadadd2  16522  saddisjlem  16526  smuval2  16544  smupvallem  16545  smu01lem  16547  smupval  16550  smueqlem  16552  smumullem  16554  bezoutlem4  16604  dfgcd2  16608  rplpwr  16620  nn0seqcvgd  16632  seq1st  16633  alginv  16637  algcvga  16641  algfx  16642  lcmf  16695  prmind2  16747  prmdvdsexp  16778  prmfac1  16783  reumodprminv  16868  pcmpt  16956  pcfac  16963  prmpwdvds  16968  prmreclem4  16983  vdwlem10  17054  ramval  17072  ramcl  17093  cshwrepswhash1  17166  prmlem1a  17170  imasleval  17599  ismre  17646  mreexexd  17708  lubprop  18416  lublecllem  18418  glbprop  18429  joinlem  18441  meetlem  18455  poslubmo  18469  posglbmo  18470  poslubd  18471  isglbd  18569  lubun  18575  mndind  18891  frmdgsum  18925  mulgnnass  19179  mhmmulg  19185  gsumwrev  19440  gsmsymgrfix  19502  gsmsymgreq  19506  psgnunilem3  19570  sylow1lem1  19672  efginvrel2  19801  efgsrel  19808  efgredlemd  19818  efgredlem  19821  efgred  19822  efgrelexlemb  19824  gsum2dlem2  20045  gsumcom2  20049  ablfac1eulem  20148  pgpfac1lem2  20151  pgpfac1lem5  20155  pgpfac1  20156  pgpfac  20160  isomnd  20197  omndadd  20202  srgmulgass  20303  srgpcomp  20304  srgbinom  20317  isdomn3  20822  isorng  20973  lmodvsmmulgdi  21027  rspprop  21379  cnfldexp  21564  ofldchr  21735  islindf4  21997  assamulgscm  22060  mplcoe1  22197  mplcoe3  22198  mplcoe5  22200  gsummoncoe1  22477  dmatval  22658  dmatel  22659  dmatmulcl  22666  pmatcoe1fsupp  22867  decpmataa0  22934  decpmatmulsumfsupp  22939  pmatcollpw2lem  22943  pm2mpmhmlem1  22984  fiinopn  23067  mretopd  23258  neiptoptop  23297  cnpfval  23400  iscnp3  23410  tgcn  23418  lmbr  23424  lmbr2  23425  lmbrf  23426  lmss  23464  ishaus  23488  hausnei2  23519  t1sep2  23535  fiuncmp  23570  dfconn2  23585  1stcfb  23611  2ndc1stc  23617  1stcrest  23619  1stcelcls  23627  1stccn  23629  lly1stc  23662  elkgen  23702  kgencn  23722  tx1stc  23816  xkopt  23821  cnmptcom  23844  isr0  23903  r0sep  23914  ptcmpfi  23979  isfildlem  24023  rnelfm  24119  fbflim  24142  flimrest  24149  isflf  24159  flffbas  24161  lmflf  24171  fclsrest  24190  isfcf  24200  cnextfvval  24231  tmdgsum  24261  eltsms  24299  tsmsi  24300  tsmsgsum  24305  tsmssubm  24309  tsmsres  24310  tsmsf1o  24311  isust  24370  isucn  24443  isucn2  24444  ucnima  24446  imasdsf1olem  24539  metss  24674  met1stc  24687  metcnp  24707  metcnpi  24710  metcnpi2  24711  metucn  24737  xrge0tsms  25001  fsumcn  25038  elcncf  25057  cncfi  25062  rescncf  25065  cncfco  25075  caucfil  25451  equivcau  25468  caubl  25476  caublcls  25477  ovolgelb  25648  ovolunlem1a  25664  ovolicc2lem3  25687  voliunlem1  25718  voliunlem3  25720  volsuplem  25723  volsup  25724  dyadmax  25766  vitali  25781  itg2leub  25902  itgfsum  25995  dvnadd  26097  dvnres  26099  cpnord  26103  dvnfre  26120  dvmptfsum  26143  dvferm1  26153  dvferm2  26155  rolle  26158  dvlip  26161  c1lip1  26165  lhop1  26182  deg1leb  26261  ply1divex  26303  fta1g  26336  plyco  26407  dgrcolem1  26439  dgrco  26441  dvnply2  26457  plydivex  26467  aalioulem2  26505  aalioulem3  26506  aalioulem5  26508  aaliou3lem2  26515  dvntaylp  26543  taylthlem1  26545  ulmdvlem3  26574  abelthlem9  26612  cxpmul2  26863  scvxcvx  27159  jensenlem2  27161  jensen  27162  wilthlem3  27243  perfectlem2  27403  bcmono  27450  bposlem5  27461  lgsquad2lem2  27558  addsq2reu  27613  2sqreulem1  27619  2sqreunnlem1  27622  dchrisumlem1  27662  dchrisum0flb  27683  pntpbnd1  27759  pntlemf  27778  qabvle  27798  qabvexp  27799  ostthlem2  27801  ostth2lem2  27807  nosupcbv  27875  nosupno  27876  nosupdm  27877  nosupfv  27879  nosupres  27880  nosupbnd1lem1  27881  nosupbnd1lem3  27883  nosupbnd1lem5  27885  noinfcbv  27890  noinfno  27891  noinfdm  27892  noinffv  27894  noinfres  27895  noinfbnd1lem3  27898  noinfbnd1lem5  27900  eqcuts2  27988  addsproplem1  28171  addsprop  28178  negsunif  28257  mulsproplem9  28326  sltmuls2  28350  precsexlem8  28416  precsexlem9  28417  precsexlem11  28419  noseqind  28494  om2noseqrdg  28506  noseqrdgfn  28508  n0addscl  28546  n0mulscl  28547  eucliddivs  28578  peano5uzs  28606  expscllem  28632  expadds  28637  expsne0  28638  expsgt0  28639  pw2cut  28662  pw2cut2  28664  bdaypw2n0bnd  28666  tgcgr4  28809  prlngmo2  29215  usgr2pth  30122  wlkiswwlks2lem4  30230  wlkiswwlks2  30233  rusgrnumwwlk  30336  clwlkclwwlklem2a  30358  clwlkclwwlklem1  30359  clwlkclwwlkfo  30369  eupth2  30599  frgr3vlem1  30633  3vfriswmgrlem  30637  3vfriswmgr  30638  wlkl0  30727  numclwlk2lem2f1o  30739  isplig  30837  isnvlem  30971  nvi  30975  nmoubi  31133  nmounbi  31137  nmblolbi  31161  ipasslem1  31192  ipassi  31202  hlim2  31553  pjhth  31754  spansni  31918  elspansn2  31928  pjige0  32052  pjcjt2  32053  pjopyth  32081  elcnop  32218  elcnfn  32243  nmopub  32269  cnopc  32274  nmfnleub  32286  elnlfn  32289  cnfnc  32291  nmbdoplb  32386  nmcexi  32387  nmcoplb  32391  lnfnmul  32409  nmbdfnlb  32411  nmcfnlb  32415  pjss2coi  32525  pjssmi  32526  isst  32574  ishst  32575  stcltr1i  32635  mdbr  32655  dmdbr  32660  mddmd2  32670  mdslmd1lem3  32688  mdslmd1lem4  32689  elat2  32701  atcvat2  32750  cdj1i  32794  iuninc  32914  fmptcof2  33011  nn0min  33174  nexple  33186  wrdt2ind  33282  ismnt  33312  xrge0tsmsd  33402  gsumwun  33405  cyc3genpm  33481  isarchi2  33514  archirng  33517  archiexdiv  33519  archiabl  33527  domnprodn0  33607  islbs5  33702  unitprodclb  33711  mxidlval  33753  1arithidom  33836  1arithufdlem3  33845  crefeq  34244  esumfzf  34468  issiga  34511  isrnsiga  34512  isldsys  34555  ismeas  34598  isrnmeas  34599  measiun  34617  eulerpartlemn  34780  sseqp1  34794  rrvsum  34853  signsply0  34947  signstfvc  34970  bnj941  35170  bnj106  35265  bnj155  35276  bnj590  35307  bnj591  35308  bnj849  35322  bnj893  35325  bnj944  35335  bnj1128  35387  r1filimi  35506  r1omhfb  35517  tz9.1regs  35555  r1omhfbregs  35558  elkarden  35576  gblacfnacd  35594  subfacp1lem6  35685  erdszelem8  35698  issconn  35726  cvmliftlem7  35791  cvmliftlem10  35794  cvmlift3lem2  35820  satfsschain  35864  satfrel  35867  satfdm  35869  satfrnmapom  35870  fmlafvel  35885  satffun  35909  mrsubvrs  36022  mclsssvlem  36062  mclsval  36063  mclsax  36069  mclsind  36070  shftvalg  36232  bccolsum  36239  iprodefisumlem  36240  faclimlem1  36243  rdgprc  36292  nmuladdss  36713  sbequbidv  36754  cbvsbdavw  36794  fveleq  36990  dfttc4lem1  37067  dfttc4  37069  elttcirr  37070  regsfromregtco  37077  mh-unprimbi  37083  unblimceq0  37124  bj-ax12  37307  bj-bm1.3ii  37728  rdgeqoa  38044  finxpreclem6  38070  domalom  38078  ralssiun  38081  wl-ax12v2cl  38180  wl-sblimt  38231  wl-sbhbt  38237  wl-2sb6d  38241  wl-mo2df  38253  wl-mo2t  38258  poimirlem2  38301  poimirlem25  38324  poimirlem28  38327  poimirlem31  38330  heicant  38334  mbfresfi  38345  itg2gt0cn  38354  sdclem2  38421  fdc  38424  seqpo  38426  incsequz  38427  mettrifi  38436  prdsbnd2  38474  heiborlem4  38493  bfplem1  38501  iscringd  38677  maxidlval  38718  igenval2  38745  iss2  39021  elrefrels3  39276  ax12eq  39743  ax12el  39744  ax12indalem  39747  ax12inda2ALT  39748  ax12inda  39750  ax12v2-o  39751  riotasvd  39758  isopos  39982  isat3  40109  ishlat1  40154  glbconN  40179  ispsubsp  40547  isldil  40912  isltrn  40921  isdilN  40956  trlval  40964  cdleme27b  41170  cdleme29b  41177  cdleme31sn1  41183  cdleme31sn1c  41190  cdleme40v  41271  cdlemk36  41715  cdlemkid5  41737  cdlemn11pre  42012  dihord2pre  42027  islpolN  42285  hdmapffval  42628  hdmapfval  42629  hdmapval2lem  42633  uzindd  42773  sticksstones1  42941  sticksstones2  42942  sticksstones3  42943  sticksstones8  42948  sticksstones10  42950  sticksstones11  42951  sticksstones12a  42952  sticksstones15  42956  indstrd  42988  unitscyglem3  42992  eu6w  43436  ismrc  43460  incssnn0  43470  mzpexpmpt  43504  pell14qrexpclnn0  43621  monotuz  43696  rmxypos  43702  jm2.17a  43715  jm2.17b  43716  rmygeid  43719  jm2.18  43743  jm2.19lem3  43746  jm2.25  43754  jm2.15nn0  43758  jm2.16nn0  43759  wepwsolem  43797  aomclem8  43816  dfac11  43817  pwslnm  43849  lnr2i  43871  hbtlem5  43883  cnsrexpcl  43920  rngunsnply  43924  unielss  43973  onsucf1lem  44024  cantnfresb  44079  onmcl  44086  naddonnn  44150  elmapintrab  44330  elmapintab  44350  cnvcnvintabd  44354  eliunov2  44433  relexpxpnnidm  44457  relexpiidm  44458  relexpss1d  44459  iunrelexpmin1  44462  relexpmulnn  44463  iunrelexpmin2  44466  relexp0a  44470  trclimalb2  44480  clsk3nimkb  44794  ntrclsiso  44821  ntrclskb  44823  ntrneiiso  44845  ntrneix2  44847  ntrneixb  44849  gneispace2  44886  gneispacess2  44900  mnuunid  45015  dvgrat  45050  pm14.122b  45161  relpeq1  45681  relpeq3  45683  trfr  45699  pwclaxpow  45721  prclaxpr  45722  uniclaxun  45723  modelac8prim  45729  permaxpow  45746  permaxpr  45747  permaxun  45748  nregmodel  45754  fnchoice  45777  fiiuncl  45813  ssinc  45833  ssdec  45834  wessf1ornlem  45931  dmrelrnrel  45970  fperiodmullem  46050  monoordxrv  46223  fmul01  46324  fmuldfeq  46327  climsuselem1  46351  climinff  46355  ellimcabssub0  46361  limcleqr  46386  addlimc  46390  0ellimcdiv  46391  limclner  46393  limsupref  46427  limsupub  46446  limsupmnf  46463  limsupre2lem  46466  limsupre2  46467  limsupre2mpt  46472  limsupre3lem  46474  limsupre3  46475  limsupre3mpt  46476  xlimbr  46569  cnrefiisplem  46571  dvnmptdivc  46680  dvnmptconst  46683  dvnmul  46685  iblspltprt  46715  itgspltprt  46721  stoweidlem2  46744  stoweidlem3  46745  stoweidlem17  46759  stoweidlem19  46761  stoweidlem21  46763  stoweidlem26  46768  fourierdlem42  46891  issal  47056  ismea  47193  isome  47236  carageniuncllem1  47263  caratheodorylem1  47268  2reu8i  47878  2reuimp0  47879  funressndmafv2rn  47988  2ffzoeq  48093  smonoord  48142  fargshiftf1  48218  ichnfimlem  48240  paireqne  48288  reupr  48299  reuopreuprim  48303  perfectALTVlem2  48515  grimcnv  48681  pgnbgreunbgrlem1  48906  pgnbgreunbgrlem4  48912  pgnbgreunbgr  48918  lmodvsmdi  49187  dmatALTval  49208  dmatALTbasel  49210  snlindsntor  49279  ldepsnlinc  49316  elbigo2r  49361  elbigolo1  49365  itcovalt2  49485  mof0  49644  isnrm4  49737  iscnrm3r  49754  iscnrm4  49760  lubsscl  49766  glbsscl  49767  ipolubdm  49793  ipoglbdm  49796  setrecseq  50491  setrec2fun  50498  setrec2lem2  50500