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  2246  axc14  2492  mojust  2563  mof  2588  eu6lem  2598  2gencl  3492  3gencl  3493  vtocl2gf  3531  vtocl3gf  3532  vtocl2g  3533  vtocl3g  3534  vtocl2ga  3537  vtocl2gaf  3538  vtocl3gaf  3539  vtocl3ga  3540  vtocl4g  3541  vtocl4ga  3542  eqeu  3664  mo2icl  3672  euind  3682  reu7  3690  reuind  3711  sbctt  3808  sbccomlem  3817  reu8nf  3824  sbcnestgfw  4379  sbcnestgf  4384  r19.36zv  4468  dedth2h  4542  dedth3h  4543  dedth4h  4544  reusngf  4635  reuprg0  4663  preq12bg  4813  elint  4913  elintrabg  4921  intab  4938  axrep1  5233  axreplem  5234  axrep2  5235  axrep6g  5245  bm1.3iiOLD  5259  reusv3  5370  swopolem  5573  solin  5590  freq1  5622  frminex  5634  vtoclr  5718  2optocl  5751  3optocl  5752  raliunxp  5819  resieq  5983  iss  6031  cnveqb  6190  reu3op  6290  reuop  6291  dfpo2  6294  preddowncl  6330  fnbrfvb  6928  fvelimab  6950  fvmptss  6999  fmptco  7123  fprg  7152  fnressn  7155  fressnfv  7157  isoselem  7342  ovg  7578  caovcan  7618  caovordig  7619  caovord  7625  tfisi  7855  tfindsg  7857  tfinds2  7860  tfinds3  7861  dfom2  7864  elom  7865  findsg  7894  finds2  7895  resf1extb  7931  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  8941  xpdom2g  9071  findcard2  9159  unfi  9165  ssfi  9167  fnfi  9172  fodomfi  9282  finsschain  9326  marypha1lem  9403  marypha1  9404  supeq1  9415  ordiso2  9487  ordtypelem7  9496  wemaplem1  9518  inf3lem2  9608  inf3lem5  9611  infdiffi  9637  cantnfval2  9648  cantnfle  9650  cantnfp1lem3  9659  oemapval  9662  cantnflem1  9668  cantnf  9672  wemapwe  9676  cnfcom  9679  cnfcom3clem  9684  ttrclss  9699  ttrclselem2  9705  tz9.1  9708  frr3g  9738  frr2  9742  r1pwALT  9828  cplem2  9891  cplem2OLD  9892  kardenOLD  9899  updjud  9939  infxpenc2lem2  10023  fseqenlem1  10027  dfac8clem  10035  alephinit  10098  dfac4  10125  dfac5lem5  10130  dfac2a  10132  dfac2b  10133  dfacacn  10144  dfac12lem3  10148  kmlem2  10154  kmlem13  10165  nnadju  10200  ackbij1lem16  10236  sornom  10279  infpssrlem4  10308  fin23lem14  10335  fin23lem32  10346  fin23lem34  10348  fin23lem36  10350  isf32lem1  10355  isf32lem2  10356  axcc2lem  10438  axcc3  10440  axcclem  10459  zornn0g  10507  ttukeylem5  10515  ttukeylem6  10516  axrepnd  10603  axpowndlem3  10608  zfcndrep  10623  fpwwe2lem7  10646  pwfseqlem3  10669  wunr1om  10728  wunfi  10730  tskr1om  10776  ingru  10824  grudomon  10826  axgroth3  10840  axgroth4  10841  nqereu  10938  mulcanenq  10969  elnp  10996  elnpi  10997  prlem934  11042  infm3  12198  nnindd  12277  nnaddcl  12280  nnmulcl  12281  nnaddcom  12284  nnne0  12294  nnadddir  12316  nnmulcom  12318  peano5uzi  12710  uzind2  12714  nn0indd  12718  zindd  12722  fzindd  12723  uzaddcl  12953  uzwo  12960  indstr  12965  zmax  12994  xmulasslem  13337  xrsupsslem  13359  xrinfmsslem  13360  xrsupss  13361  xrinfmss  13362  flval2  13875  om2uzlti  14014  uzrdgfni  14022  rabssnn0fi  14050  mptnn0fsupp  14061  seqcl2  14084  seqfveq2  14088  seqshft2  14092  monoord  14096  seqsplit  14099  seqcaopr3  14101  seqf1olem2a  14104  seqf1o  14107  seqid2  14112  seqhomo  14113  ser1const  14122  expcllem  14136  expeq0  14156  mulexp  14165  expadd  14168  expmul  14171  expmordi  14231  leexp2r  14238  leexp1a  14239  bernneq  14293  modexp  14302  facdiv  14351  faclbnd  14354  faclbnd4lem4  14360  hashgadd  14441  hashxp  14499  hashmap  14500  hashf1lem2  14521  hashf1  14522  seqcoll  14529  wrdind  14791  wrd2ind  14792  pfxccatin12lem3  14801  cshweqrep  14892  2cshwcshw  14896  relexp0g  15095  relexpsucnnr  15098  relexpsucnnl  15103  relexpcnv  15108  relexpnndm  15114  relexpaddnn  15124  rtrclreclem1  15130  dfrtrclrec2  15131  rtrclreclem2  15132  rtrclreclem4  15134  dfrtrcl2  15135  relexpind  15137  reusq0  15552  rlim  15582  rlim2  15583  rlim0  15595  rlim0lt  15596  rlimi  15600  ello12r  15604  ello1mpt  15608  ello1d  15610  elo12r  15615  lo1o1  15619  o1lo1  15624  lo1res  15646  climshft  15663  o1compt  15674  rlimo1  15704  lo1add  15714  lo1mul  15715  rlimdiv  15733  climub  15749  climserle  15750  caucvgrlem  15760  caurcvgr  15761  iseraltlem2  15770  summolem2a  15801  sumss  15810  fsum2d  15857  fsumabs  15888  fsumrlim  15898  fsumo1  15899  fsumiun  15908  binom  15919  climcndslem1  15938  climcndslem2  15939  cvgrat  15972  clim2prod  15977  prodfn0  15983  prodfrec  15984  ntrivcvgfvn0  15988  prodmolem2a  16021  fprodabs  16061  fprodn0  16066  fprod2d  16068  binomfallfac  16127  bpolycl  16138  bpolydif  16141  fprodefsum  16181  demoivreALT  16289  ruclem8  16325  ruclem9  16326  dvdsle  16400  dvdsfac  16416  divalglem7  16489  bitsinv1  16532  sadcadd  16548  sadadd2  16550  saddisjlem  16554  smuval2  16572  smupvallem  16573  smu01lem  16575  smupval  16578  smueqlem  16580  smumullem  16582  bezoutlem4  16632  dfgcd2  16636  rplpwr  16648  nn0seqcvgd  16660  seq1st  16661  alginv  16665  algcvga  16669  algfx  16670  lcmf  16723  prmind2  16775  prmdvdsexp  16806  prmfac1  16811  reumodprminv  16896  pcmpt  16984  pcfac  16991  prmpwdvds  16996  prmreclem4  17011  vdwlem10  17082  ramval  17100  ramcl  17121  cshwrepswhash1  17194  prmlem1a  17198  imasleval  17627  ismre  17674  mreexexd  17736  lubprop  18444  lublecllem  18446  glbprop  18457  joinlem  18469  meetlem  18483  poslubmo  18497  posglbmo  18498  poslubd  18499  isglbd  18597  lubun  18603  mndind  18937  frmdgsum  18971  mulgnnass  19232  mhmmulg  19238  gsumwrev  19493  gsmsymgrfix  19555  gsmsymgreq  19559  psgnunilem3  19623  sylow1lem1  19725  efginvrel2  19854  efgsrel  19861  efgredlemd  19871  efgredlem  19874  efgred  19875  efgrelexlemb  19877  gsum2dlem2  20098  gsumcom2  20102  ablfac1eulem  20201  pgpfac1lem2  20204  pgpfac1lem5  20208  pgpfac1  20209  pgpfac  20213  isomnd  20250  omndadd  20255  srgmulgass  20356  srgpcomp  20357  srgbinom  20370  isdomn3  20876  isorng  21027  lmodvsmmulgdi  21081  rspprop  21433  cnfldexp  21618  ofldchr  21789  islindf4  22051  assamulgscm  22116  mplcoe1  22253  mplcoe3  22254  mplcoe5  22256  gsummoncoe1  22533  dmatval  22714  dmatel  22715  dmatmulcl  22722  pmatcoe1fsupp  22926  decpmataa0  22993  decpmatmulsumfsupp  22998  pmatcollpw2lem  23002  pm2mpmhmlem1  23043  fiinopn  23126  mretopd  23317  neiptoptop  23356  cnpfval  23459  iscnp3  23469  tgcn  23477  lmbr  23483  lmbr2  23484  lmbrf  23485  lmss  23523  ishaus  23547  hausnei2  23578  t1sep2  23594  fiuncmp  23629  dfconn2  23644  1stcfb  23670  2ndc1stc  23676  1stcrest  23678  1stcelcls  23687  1stccn  23689  lly1stc  23722  elkgen  23762  kgencn  23782  tx1stc  23876  xkopt  23881  cnmptcom  23904  isr0  23963  r0sep  23974  ptcmpfi  24039  isfildlem  24083  rnelfm  24179  fbflim  24202  flimrest  24209  isflf  24219  flffbas  24221  lmflf  24231  fclsrest  24250  isfcf  24260  cnextfvval  24291  tmdgsum  24321  eltsms  24359  tsmsi  24360  tsmsgsum  24365  tsmssubm  24369  tsmsres  24370  tsmsf1o  24371  isust  24430  isucn  24503  isucn2  24504  ucnima  24506  imasdsf1olem  24599  metss  24734  met1stc  24747  metcnp  24767  metcnpi  24770  metcnpi2  24771  metucn  24797  xrge0tsms  25061  fsumcn  25098  elcncf  25117  cncfi  25122  rescncf  25125  cncfco  25135  caucfil  25511  equivcau  25528  caubl  25536  caublcls  25537  ovolgelb  25708  ovolunlem1a  25724  ovolicc2lem3  25747  voliunlem1  25778  voliunlem3  25780  volsuplem  25783  volsup  25784  dyadmax  25826  vitali  25841  itg2leub  25962  itgfsum  26054  dvnadd  26156  dvnres  26158  cpnord  26162  dvnfre  26179  dvmptfsum  26202  dvferm1  26212  dvferm2  26214  rolle  26217  dvlip  26220  c1lip1  26224  lhop1  26241  deg1leb  26320  ply1divex  26362  fta1g  26395  plyco  26467  dgrcolem1  26499  dgrco  26501  dvnply2  26517  plydivex  26527  aalioulem2  26569  aalioulem3  26570  aalioulem5  26572  aaliou3lem2  26579  dvntaylp  26607  taylthlem1  26609  ulmdvlem3  26638  abelthlem9  26676  cxpmul2  26926  scvxcvx  27222  jensenlem2  27224  jensen  27225  wilthlem3  27306  perfectlem2  27466  bcmono  27513  bposlem5  27524  lgsquad2lem2  27621  addsq2reu  27676  2sqreulem1  27682  2sqreunnlem1  27685  dchrisumlem1  27725  dchrisum0flb  27746  pntpbnd1  27822  pntlemf  27841  qabvle  27861  qabvexp  27862  ostthlem2  27864  ostth2lem2  27870  nosupcbv  27938  nosupno  27939  nosupdm  27940  nosupfv  27942  nosupres  27943  nosupbnd1lem1  27944  nosupbnd1lem3  27946  nosupbnd1lem5  27948  noinfcbv  27953  noinfno  27954  noinfdm  27955  noinffv  27957  noinfres  27958  noinfbnd1lem3  27961  noinfbnd1lem5  27963  eqcuts2  28051  addsproplem1  28234  addsprop  28241  negsunif  28320  mulsproplem9  28389  sltmuls2  28413  precsexlem8  28479  precsexlem9  28480  precsexlem11  28482  noseqind  28557  om2noseqrdg  28569  noseqrdgfn  28571  n0addscl  28609  n0mulscl  28610  eucliddivs  28641  peano5uzs  28669  expscllem  28695  expadds  28700  expsne0  28701  expsgt0  28702  pw2cut  28725  pw2cut2  28727  bdaypw2n0bnd  28729  tgcgr4  28873  prlngmo2  29313  usgr2pth  30229  wlkiswwlks2lem4  30340  wlkiswwlks2  30343  rusgrnumwwlk  30446  clwlkclwwlklem2a  30468  clwlkclwwlklem1  30469  clwlkclwwlkfo  30479  eupth2  30719  frgr3vlem1  30753  3vfriswmgrlem  30757  3vfriswmgr  30758  wlkl0  30847  numclwlk2lem2f1o  30859  isplig  30957  isnvlem  31091  nvi  31095  nmoubi  31253  nmounbi  31257  nmblolbi  31281  ipasslem1  31312  ipassi  31322  hlim2  31673  pjhth  31874  spansni  32038  elspansn2  32048  pjige0  32172  pjcjt2  32173  pjopyth  32201  elcnop  32338  elcnfn  32363  nmopub  32389  cnopc  32394  nmfnleub  32406  elnlfn  32409  cnfnc  32411  nmbdoplb  32506  nmcexi  32507  nmcoplb  32511  lnfnmul  32529  nmbdfnlb  32531  nmcfnlb  32535  pjss2coi  32645  pjssmi  32646  isst  32694  ishst  32695  stcltr1i  32755  mdbr  32775  dmdbr  32780  mddmd2  32790  mdslmd1lem3  32808  mdslmd1lem4  32809  elat2  32821  atcvat2  32870  cdj1i  32914  iuninc  33034  fmptcof2  33130  nn0min  33291  nexple  33303  wrdt2ind  33395  ismnt  33423  xrge0tsmsd  33513  gsumwun  33516  cyc3genpm  33592  isarchi2  33625  archirng  33628  archiexdiv  33630  archiabl  33638  domnprodn0  33718  islbs5  33813  unitprodclb  33822  mxidlval  33864  1arithidom  33947  1arithufdlem3  33956  crefeq  34355  esumfzf  34579  issiga  34622  isrnsiga  34623  isldsys  34667  ismeas  34710  isrnmeas  34711  measiun  34729  eulerpartlemn  34892  sseqp1  34906  rrvsum  34965  signsply0  35059  signstfvc  35082  bnj941  35282  bnj106  35377  bnj155  35388  bnj590  35419  bnj591  35420  bnj849  35434  bnj893  35437  bnj944  35447  bnj1128  35499  r1filimi  35611  r1omhfb  35622  tz9.1regs  35660  r1omhfbregs  35663  elkarden  35681  gblacfnacd  35699  subfacp1lem6  35764  erdszelem8  35777  issconn  35805  cvmliftlem7  35870  cvmliftlem10  35873  cvmlift3lem2  35899  satfsschain  35943  satfrel  35946  satfdm  35948  satfrnmapom  35949  fmlafvel  35964  satffun  35988  mrsubvrs  36101  mclsssvlem  36141  mclsval  36142  mclsax  36148  mclsind  36149  shftvalg  36311  bccolsum  36318  iprodefisumlem  36319  faclimlem1  36322  rdgprc  36371  nmuladdss  36793  sbequbidv  36834  cbvsbdavw  36874  fveleq  37070  dfttc4lem1  37147  dfttc4  37149  elttcirr  37150  regsfromregtco  37157  mh-unprimbi  37163  unblimceq0  37204  bj-ax12  37387  bj-bm1.3ii  37808  rdgeqoa  38124  finxpreclem6  38150  domalom  38158  ralssiun  38161  wl-ax12v2cl  38260  wl-sblimt  38311  wl-sbhbt  38317  wl-2sb6d  38321  wl-mo2df  38333  wl-mo2t  38338  poimirlem2  38371  poimirlem25  38394  poimirlem28  38397  poimirlem31  38400  heicant  38404  mbfresfi  38415  itg2gt0cn  38424  sdclem2  38492  fdc  38495  seqpo  38497  incsequz  38498  mettrifi  38507  prdsbnd2  38545  heiborlem4  38564  bfplem1  38572  iscringd  38748  maxidlval  38789  igenval2  38816  iss2  39092  elrefrels3  39347  ax12eq  39814  ax12el  39815  ax12indalem  39818  ax12inda2ALT  39819  ax12inda  39821  ax12v2-o  39822  riotasvd  39829  isopos  40053  isat3  40180  ishlat1  40225  glbconN  40250  ispsubsp  40618  isldil  40983  isltrn  40992  isdilN  41027  trlval  41035  cdleme27b  41241  cdleme29b  41248  cdleme31sn1  41254  cdleme31sn1c  41261  cdleme40v  41342  cdlemk36  41786  cdlemkid5  41808  cdlemn11pre  42083  dihord2pre  42098  islpolN  42356  hdmapffval  42699  hdmapfval  42700  hdmapval2lem  42704  uzindd  42844  sticksstones1  43012  sticksstones2  43013  sticksstones3  43014  sticksstones8  43019  sticksstones10  43021  sticksstones11  43022  sticksstones12a  43023  sticksstones15  43027  indstrd  43059  unitscyglem3  43063  eu6w  43522  ismrc  43546  incssnn0  43556  mzpexpmpt  43590  pell14qrexpclnn0  43707  monotuz  43782  rmxypos  43788  jm2.17a  43801  jm2.17b  43802  rmygeid  43805  jm2.18  43829  jm2.19lem3  43832  jm2.25  43840  jm2.15nn0  43844  jm2.16nn0  43845  wepwsolem  43883  aomclem8  43902  dfac11  43903  pwslnm  43935  lnr2i  43957  hbtlem5  43969  cnsrexpcl  44006  rngunsnply  44010  unielss  44059  onsucf1lem  44110  cantnfresb  44165  onmcl  44172  naddonnn  44236  elmapintrab  44416  elmapintab  44436  cnvcnvintabd  44440  eliunov2  44519  relexpxpnnidm  44543  relexpiidm  44544  relexpss1d  44545  iunrelexpmin1  44548  relexpmulnn  44549  iunrelexpmin2  44552  relexp0a  44556  trclimalb2  44566  clsk3nimkb  44880  ntrclsiso  44907  ntrclskb  44909  ntrneiiso  44931  ntrneix2  44933  ntrneixb  44935  gneispace2  44972  gneispacess2  44986  mnuunid  45101  dvgrat  45136  pm14.122b  45247  relpeq1  45767  relpeq3  45769  trfr  45785  pwclaxpow  45807  prclaxpr  45808  uniclaxun  45809  modelac8prim  45815  permaxpow  45832  permaxpr  45833  permaxun  45834  nregmodel  45840  fnchoice  45863  fiiuncl  45899  ssinc  45919  ssdec  45920  wessf1ornlem  46017  dmrelrnrel  46056  fperiodmullem  46136  monoordxrv  46309  fmul01  46410  fmuldfeq  46413  climsuselem1  46437  climinff  46441  ellimcabssub0  46447  limcleqr  46472  addlimc  46476  0ellimcdiv  46477  limclner  46479  limsupref  46513  limsupub  46532  limsupmnf  46549  limsupre2lem  46552  limsupre2  46553  limsupre2mpt  46558  limsupre3lem  46560  limsupre3  46561  limsupre3mpt  46562  xlimbr  46655  cnrefiisplem  46657  dvnmptdivc  46766  dvnmptconst  46769  dvnmul  46771  iblspltprt  46801  itgspltprt  46807  stoweidlem2  46830  stoweidlem3  46831  stoweidlem17  46845  stoweidlem19  46847  stoweidlem21  46849  stoweidlem26  46854  fourierdlem42  46977  issal  47142  ismea  47279  isome  47322  carageniuncllem1  47349  caratheodorylem1  47354  2reu8i  48001  2reuimp0  48002  funressndmafv2rn  48111  2ffzoeq  48216  smonoord  48265  fargshiftf1  48341  ichnfimlem  48363  paireqne  48411  reupr  48422  reuopreuprim  48426  perfectALTVlem2  48638  grimcnv  48804  pgnbgreunbgrlem1  49029  pgnbgreunbgrlem4  49035  pgnbgreunbgr  49041  lmodvsmdi  49309  dmatALTval  49330  dmatALTbasel  49332  snlindsntor  49401  ldepsnlinc  49438  elbigo2r  49483  elbigolo1  49487  itcovalt2  49607  mof0  49766  isnrm4  49857  iscnrm3r  49874  iscnrm4  49880  lubsscl  49886  glbsscl  49887  ipolubdm  49913  ipoglbdm  49916  setrecseq  50611  setrec2fun  50618  setrec2lem2  50620