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  2247  axc14  2493  mojust  2564  mof  2589  eu6lem  2599  2gencl  3493  3gencl  3494  vtocl2gf  3532  vtocl3gf  3533  vtocl2g  3534  vtocl3g  3535  vtocl2ga  3538  vtocl2gaf  3539  vtocl3gaf  3540  vtocl3ga  3541  vtocl4g  3542  vtocl4ga  3543  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  5243  reusv3  5367  swopolem  5569  solin  5586  freq1  5618  frminex  5630  vtoclr  5714  2optocl  5747  3optocl  5748  raliunxp  5816  resieq  5981  iss  6027  cnveqb  6189  reu3op  6294  reuop  6295  dfpo2  6298  preddowncl  6334  fnbrfvb  6933  fvelimab  6955  fvmptss  7004  fmptco  7128  fprg  7157  fnressn  7160  fressnfv  7162  isoselem  7347  ovg  7583  caovcan  7623  caovordig  7624  caovord  7630  tfisi  7868  tfindsg  7870  tfinds2  7873  tfinds3  7874  dfom2  7877  elom  7878  findsg  7907  finds2  7908  resf1extb  7944  f1o2ndf1  8131  poxp  8138  fnse  8143  xpord3inddlem  8164  soseq  8169  fpr3g  8296  frrlem12  8308  fpr2a  8313  wfr3g  8330  smoeq  8351  smores  8353  smogt  8368  tfrlem1  8376  tfr3  8400  tz7.48lem  8443  oaordi  8547  oeordi  8589  oeoa  8599  oeoe  8601  nnacl  8613  nnmcl  8614  nnecl  8615  nnacom  8619  nnaordi  8620  nnawordi  8623  nnaass  8624  nndi  8625  nnmass  8626  nnmsucr  8627  nnmcom  8628  nnmordi  8633  naddssim  8688  naddoa  8705  2ecoptocl  8822  3ecoptocl  8823  undifixp  8955  xpdom2g  9085  findcard2  9173  unfi  9179  ssfi  9181  fnfi  9186  fodomfi  9297  finsschain  9341  marypha1lem  9418  marypha1  9419  supeq1  9430  ordiso2  9502  ordtypelem7  9511  wemaplem1  9533  inf3lem2  9623  inf3lem5  9626  infdiffi  9652  cantnfval2  9663  cantnfle  9665  cantnfp1lem3  9674  oemapval  9677  cantnflem1  9683  cantnf  9687  wemapwe  9691  cnfcom  9694  cnfcom3clem  9699  ttrclss  9714  ttrclselem2  9720  tz9.1  9723  frr3g  9753  frr2  9757  r1pwALT  9853  r1filimi  9896  cplem2  9945  cplem2OLD  9946  kardenOLD  9953  setrec2fun  9966  setrec2lem2  9969  updjud  10008  infxpenc2lem2  10092  fseqenlem1  10096  dfac8clem  10104  alephinit  10167  dfac4  10194  dfac5lem5  10199  dfac2a  10201  dfac2b  10202  dfacacn  10213  dfac12lem3  10217  kmlem2  10223  kmlem13  10234  nnadju  10269  ackbij1lem16  10305  sornom  10348  infpssrlem4  10377  fin23lem14  10404  fin23lem32  10415  fin23lem34  10417  fin23lem36  10419  isf32lem1  10424  isf32lem2  10425  axcc2lem  10507  axcc3  10509  axcclem  10528  zornn0g  10576  ttukeylem5  10584  ttukeylem6  10585  axrepnd  10672  axpowndlem3  10677  zfcndrep  10692  fpwwe2lem7  10715  pwfseqlem3  10738  wunr1om  10797  wunfi  10799  tskr1om  10845  ingru  10893  grudomon  10895  axgroth3  10909  axgroth4  10910  nqereu  11007  mulcanenq  11038  elnp  11065  elnpi  11066  prlem934  11111  infm3  12269  nnindd  12348  nnaddcl  12351  nnmulcl  12352  nnaddcom  12355  nnne0  12365  nnadddir  12387  nnmulcom  12389  peano5uzi  12781  uzind2  12785  nn0indd  12789  zindd  12793  fzindd  12794  uzaddcl  13024  uzwo  13031  indstr  13036  zmax  13065  xmulasslem  13408  xrsupsslem  13430  xrinfmsslem  13431  xrsupss  13432  xrinfmss  13433  flval2  13947  om2uzlti  14086  uzrdgfni  14094  rabssnn0fi  14122  mptnn0fsupp  14133  seqcl2  14156  seqfveq2  14160  seqshft2  14164  monoord  14168  seqsplit  14171  seqcaopr3  14173  seqf1olem2a  14176  seqf1o  14179  seqid2  14184  seqhomo  14185  ser1const  14194  expcllem  14208  expeq0  14228  mulexp  14237  expadd  14240  expmul  14243  expmordi  14303  leexp2r  14310  leexp1a  14311  bernneq  14366  modexp  14375  facdiv  14424  faclbnd  14427  faclbnd4lem4  14433  hashgadd  14514  hashxp  14572  hashmap  14573  hashf1lem2  14594  hashf1  14595  seqcoll  14602  wrdind  14864  wrd2ind  14865  pfxccatin12lem3  14874  cshweqrep  14965  2cshwcshw  14969  relexp0g  15168  relexpsucnnr  15171  relexpsucnnl  15176  relexpcnv  15181  relexpnndm  15187  relexpaddnn  15197  rtrclreclem1  15203  dfrtrclrec2  15204  rtrclreclem2  15205  rtrclreclem4  15207  dfrtrcl2  15208  relexpind  15210  reusq0  15625  rlim  15655  rlim2  15656  rlim0  15668  rlim0lt  15669  rlimi  15673  ello12r  15677  ello1mpt  15681  ello1d  15683  elo12r  15688  lo1o1  15692  o1lo1  15697  lo1res  15719  climshft  15736  o1compt  15747  rlimo1  15777  lo1add  15787  lo1mul  15788  rlimdiv  15806  climub  15822  climserle  15823  caucvgrlem  15833  caurcvgr  15834  iseraltlem2  15843  summolem2a  15874  sumss  15883  fsum2d  15930  fsumabs  15961  fsumrlim  15971  fsumo1  15972  fsumiun  15981  binom  15992  climcndslem1  16011  climcndslem2  16012  cvgrat  16045  clim2prod  16050  prodfn0  16056  prodfrec  16057  ntrivcvgfvn0  16061  prodmolem2a  16094  fprodabs  16134  fprodn0  16139  fprod2d  16141  binomfallfac  16200  bpolycl  16211  bpolydif  16214  fprodefsum  16254  demoivreALT  16362  ruclem8  16398  ruclem9  16399  dvdsle  16473  dvdsfac  16489  divalglem7  16562  bitsinv1  16605  sadcadd  16621  sadadd2  16623  saddisjlem  16627  smuval2  16645  smupvallem  16646  smu01lem  16648  smupval  16651  smueqlem  16653  smumullem  16655  bezoutlem4  16708  dfgcd2  16712  rplpwr  16725  nn0seqcvgd  16738  seq1st  16739  alginv  16743  algcvga  16747  algfx  16748  lcmf  16801  prmind2  16853  prmdvdsexp  16884  prmfac1  16889  reumodprminv  16975  pcmpt  17063  pcfac  17070  prmpwdvds  17075  prmreclem4  17090  vdwlem10  17161  ramval  17179  ramcl  17200  cshwrepswhash1  17273  prmlem1a  17277  imasleval  17706  ismre  17753  mreexexd  17815  lubprop  18523  lublecllem  18525  glbprop  18536  joinlem  18548  meetlem  18562  poslubmo  18576  posglbmo  18577  poslubd  18578  isglbd  18676  lubun  18682  mndind  19017  frmdgsum  19051  mulgnnass  19312  mhmmulg  19318  gsumwrev  19573  gsmsymgrfix  19635  gsmsymgreq  19639  psgnunilem3  19703  sylow1lem1  19805  efginvrel2  19934  efgsrel  19941  efgredlemd  19951  efgredlem  19954  efgred  19955  efgrelexlemb  19957  gsum2dlem2  20178  gsumcom2  20182  ablfac1eulem  20281  pgpfac1lem2  20284  pgpfac1lem5  20288  pgpfac1  20289  pgpfac  20293  isomnd  20330  omndadd  20335  srgmulgass  20436  srgpcomp  20437  srgbinom  20450  isdomn3  20959  isorng  21111  lmodvsmmulgdi  21165  rspprop  21517  cnfldexp  21704  ofldchr  21875  islindf4  22137  assamulgscm  22202  mplcoe1  22339  mplcoe3  22340  mplcoe5  22342  gsummoncoe1  22619  dmatval  22800  dmatel  22801  dmatmulcl  22808  pmatcoe1fsupp  23012  decpmataa0  23079  decpmatmulsumfsupp  23084  pmatcollpw2lem  23088  pm2mpmhmlem1  23129  fiinopn  23212  mretopd  23403  neiptoptop  23442  cnpfval  23545  iscnp3  23555  tgcn  23563  lmbr  23569  lmbr2  23570  lmbrf  23571  lmss  23609  ishaus  23633  hausnei2  23664  t1sep2  23680  fiuncmp  23715  dfconn2  23730  1stcfb  23756  2ndc1stc  23762  1stcrest  23764  1stcelcls  23773  1stccn  23775  lly1stc  23808  elkgen  23848  kgencn  23868  tx1stc  23962  xkopt  23967  cnmptcom  23990  isr0  24049  r0sep  24060  ptcmpfi  24125  isfildlem  24169  rnelfm  24265  fbflim  24288  flimrest  24295  isflf  24305  flffbas  24307  lmflf  24317  fclsrest  24336  isfcf  24346  cnextfvval  24377  tmdgsum  24407  eltsms  24445  tsmsi  24446  tsmsgsum  24451  tsmssubm  24455  tsmsres  24456  tsmsf1o  24457  isust  24516  isucn  24589  isucn2  24590  ucnima  24592  imasdsf1olem  24685  metss  24820  met1stc  24833  metcnp  24853  metcnpi  24856  metcnpi2  24857  metucn  24883  xrge0tsms  25147  fsumcn  25184  elcncf  25203  cncfi  25208  rescncf  25211  cncfco  25221  caucfil  25597  equivcau  25614  caubl  25622  caublcls  25623  ovolgelb  25794  ovolunlem1a  25810  ovolicc2lem3  25833  voliunlem1  25864  voliunlem3  25866  volsuplem  25869  volsup  25870  dyadmax  25912  vitali  25927  itg2leub  26048  itgfsum  26140  dvnadd  26242  dvnres  26244  cpnord  26248  dvnfre  26265  dvmptfsum  26288  dvferm1  26298  dvferm2  26300  rolle  26303  dvlip  26306  c1lip1  26310  lhop1  26327  deg1leb  26406  ply1divex  26448  fta1g  26481  plyco  26553  dgrcolem1  26585  dgrco  26587  dvnply2  26601  plydivex  26611  aalioulem2  26653  aalioulem3  26654  aalioulem5  26656  aaliou3lem2  26663  dvntaylp  26691  taylthlem1  26693  ulmdvlem3  26722  abelthlem9  26760  cxpmul2  27010  scvxcvx  27306  jensenlem2  27308  jensen  27309  wilthlem3  27390  perfectlem2  27550  bcmono  27597  bposlem5  27608  lgsquad2lem2  27705  addsq2reu  27760  2sqreulem1  27766  2sqreunnlem1  27769  dchrisumlem1  27809  dchrisum0flb  27830  pntpbnd1  27906  pntlemf  27925  qabvle  27945  qabvexp  27946  ostthlem2  27948  ostth2lem2  27954  fltoprm  27988  nosupcbv  28052  nosupno  28053  nosupdm  28054  nosupfv  28056  nosupres  28057  nosupbnd1lem1  28058  nosupbnd1lem3  28060  nosupbnd1lem5  28062  noinfcbv  28067  noinfno  28068  noinfdm  28069  noinffv  28071  noinfres  28072  noinfbnd1lem3  28075  noinfbnd1lem5  28077  eqcuts2  28165  addsproplem1  28348  addsprop  28355  negsunif  28434  mulsproplem9  28503  sltmuls2  28527  precsexlem8  28593  precsexlem9  28594  precsexlem11  28596  noseqind  28671  om2noseqrdg  28683  noseqrdgfn  28685  n0addscl  28723  n0mulscl  28724  eucliddivs  28755  peano5uzs  28783  expscllem  28809  expadds  28814  expsne0  28815  expsgt0  28816  pw2cut  28839  pw2cut2  28841  bdaypw2n0bnd  28843  tgcgr4  28987  prlngmo2  29427  usgr2pth  30343  wlkiswwlks2lem4  30454  wlkiswwlks2  30457  rusgrnumwwlk  30560  clwlkclwwlklem2a  30582  clwlkclwwlklem1  30583  clwlkclwwlkfo  30593  eupth2  30833  frgr3vlem1  30867  3vfriswmgrlem  30871  3vfriswmgr  30872  wlkl0  30961  numclwlk2lem2f1o  30973  isplig  31071  isnvlem  31205  nvi  31209  nmoubi  31367  nmounbi  31371  nmblolbi  31395  ipasslem1  31426  ipassi  31436  hlim2  31787  pjhth  31988  spansni  32152  elspansn2  32162  pjige0  32286  pjcjt2  32287  pjopyth  32315  elcnop  32452  elcnfn  32477  nmopub  32503  cnopc  32508  nmfnleub  32520  elnlfn  32523  cnfnc  32525  nmbdoplb  32620  nmcexi  32621  nmcoplb  32625  lnfnmul  32643  nmbdfnlb  32645  nmcfnlb  32649  pjss2coi  32759  pjssmi  32760  isst  32808  ishst  32809  stcltr1i  32869  mdbr  32889  dmdbr  32894  mddmd2  32904  mdslmd1lem3  32922  mdslmd1lem4  32923  elat2  32935  atcvat2  32984  cdj1i  33028  iuninc  33148  fmptcof2  33244  nn0min  33405  nexple  33417  wrdt2ind  33509  ismnt  33537  xrge0tsmsd  33627  gsumwun  33630  cyc3genpm  33706  isarchi2  33739  archirng  33742  archiexdiv  33744  archiabl  33752  domnprodn0  33832  islbs5  33928  unitprodclb  33937  mxidlval  33979  1arithidom  34062  1arithufdlem3  34071  crefeq  34470  esumfzf  34694  issiga  34737  isrnsiga  34738  isldsys  34782  ismeas  34825  isrnmeas  34826  measiun  34844  eulerpartlemn  35006  sseqp1  35020  rrvsum  35079  signsply0  35173  signstfvc  35196  bnj941  35396  bnj106  35491  bnj155  35502  bnj590  35533  bnj591  35534  bnj849  35548  bnj893  35551  bnj944  35561  bnj1128  35613  r1omhfb  35727  tz9.1regs  35785  r1omhfbregs  35788  elkarden  35806  gblacfnacd  35864  subfacp1lem6  35929  erdszelem8  35942  issconn  35970  cvmliftlem7  36035  cvmliftlem10  36038  cvmlift3lem2  36064  satfsschain  36108  satfrel  36111  satfdm  36113  satfrnmapom  36114  fmlafvel  36129  satffun  36153  mrsubvrs  36266  mclsssvlem  36306  mclsval  36307  mclsax  36313  mclsind  36314  shftvalg  36476  bccolsum  36483  iprodefisumlem  36484  faclimlem1  36487  rdgprc  36536  nmuladdss  36942  sbequbidv  36983  cbvsbdavw  37023  fveleq  37219  dfttc4lem1  37296  dfttc4  37298  elttcirr  37299  regsfromregtco  37306  mh-unprimbi  37312  unblimceq0  37353  bj-ax12  37536  bj-bm1.3ii  37959  rdgeqoa  38273  finxpreclem6  38299  domalom  38307  ralssiun  38310  wl-ax12v2cl  38409  wl-sblimt  38460  wl-sbhbt  38466  wl-2sb6d  38470  wl-mo2df  38482  wl-mo2t  38487  poimirlem2  38520  poimirlem25  38543  poimirlem28  38546  poimirlem31  38549  heicant  38553  mbfresfi  38564  itg2gt0cn  38573  sdclem2  38656  fdc  38659  seqpo  38661  incsequz  38662  mettrifi  38671  prdsbnd2  38709  heiborlem4  38728  bfplem1  38736  iscringd  38912  maxidlval  38953  igenval2  38980  iss2  39256  elrefrels3  39511  ax12eq  39978  ax12el  39979  ax12indalem  39982  ax12inda2ALT  39983  ax12inda  39985  ax12v2-o  39986  riotasvd  39993  isopos  40217  isat3  40344  ishlat1  40389  glbconN  40414  ispsubsp  40782  isldil  41147  isltrn  41156  isdilN  41191  trlval  41199  cdleme27b  41405  cdleme29b  41412  cdleme31sn1  41418  cdleme31sn1c  41425  cdleme40v  41506  cdlemk36  41950  cdlemkid5  41972  cdlemn11pre  42247  dihord2pre  42262  islpolN  42520  hdmapffval  42863  hdmapfval  42864  hdmapval2lem  42868  uzindd  43008  sticksstones1  43176  sticksstones2  43177  sticksstones3  43178  sticksstones8  43183  sticksstones10  43185  sticksstones11  43186  sticksstones12a  43187  sticksstones15  43191  indstrd  43223  unitscyglem3  43227  eu6w  43667  ismrc  43691  incssnn0  43701  mzpexpmpt  43735  pell14qrexpclnn0  43852  monotuz  43927  rmxypos  43933  jm2.17a  43946  jm2.17b  43947  rmygeid  43950  jm2.18  43974  jm2.19lem3  43977  jm2.25  43985  jm2.15nn0  43989  jm2.16nn0  43990  wepwsolem  44028  aomclem8  44047  dfac11  44048  pwslnm  44080  lnr2i  44102  hbtlem5  44114  cnsrexpcl  44151  rngunsnply  44155  unielss  44204  onsucf1lem  44255  cantnfresb  44310  onmcl  44317  naddonnn  44381  elmapintrab  44561  elmapintab  44581  cnvcnvintabd  44585  eliunov2  44664  relexpxpnnidm  44688  relexpiidm  44689  relexpss1d  44690  iunrelexpmin1  44693  relexpmulnn  44694  iunrelexpmin2  44697  relexp0a  44701  trclimalb2  44711  clsk3nimkb  45025  ntrclsiso  45052  ntrclskb  45054  ntrneiiso  45076  ntrneix2  45078  ntrneixb  45080  gneispace2  45117  gneispacess2  45131  mnuunid  45246  dvgrat  45281  pm14.122b  45392  relpeq1  45912  relpeq3  45914  trfr  45930  pwclaxpow  45952  prclaxpr  45953  uniclaxun  45954  modelac8prim  45960  permaxpow  45977  permaxpr  45978  permaxun  45979  nregmodel  45985  fnchoice  46015  fiiuncl  46051  ssinc  46071  ssdec  46072  wessf1ornlem  46169  dmrelrnrel  46208  fperiodmullem  46288  monoordxrv  46460  fmul01  46561  fmuldfeq  46564  climsuselem1  46588  climinff  46592  ellimcabssub0  46598  limcleqr  46623  addlimc  46627  0ellimcdiv  46628  limclner  46630  limsupref  46664  limsupub  46683  limsupmnf  46700  limsupre2lem  46703  limsupre2  46704  limsupre2mpt  46709  limsupre3lem  46711  limsupre3  46712  limsupre3mpt  46713  xlimbr  46806  cnrefiisplem  46808  dvnmptdivc  46917  dvnmptconst  46920  dvnmul  46922  iblspltprt  46952  itgspltprt  46958  stoweidlem2  46981  stoweidlem3  46982  stoweidlem17  46996  stoweidlem19  46998  stoweidlem21  47000  stoweidlem26  47005  fourierdlem42  47128  issal  47293  ismea  47430  isome  47473  carageniuncllem1  47500  caratheodorylem1  47505  2reu8i  48152  2reuimp0  48153  funressndmafv2rn  48262  2ffzoeq  48367  smonoord  48416  fargshiftf1  48492  ichnfimlem  48514  paireqne  48562  reupr  48573  reuopreuprim  48577  perfectALTVlem2  48789  grimcnv  48955  pgnbgreunbgrlem1  49180  pgnbgreunbgrlem4  49186  pgnbgreunbgr  49192  lmodvsmdi  49460  dmatALTval  49481  dmatALTbasel  49483  snlindsntor  49552  ldepsnlinc  49589  elbigo2r  49634  elbigolo1  49638  itcovalt2  49758  mof0  49917  isnrm4  50008  iscnrm3r  50025  iscnrm4  50031  lubsscl  50037  glbsscl  50038  ipolubdm  50064  ipoglbdm  50067  setrecseq  50757