Theorem imbi2d 339

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  imbi12d  343  imbi2  347  pm5.42  542  orbi2d  912  19.23t  2201  axc14  2460  mojust  2531  mof  2555  eu6lem  2565  nfabdwOLD  2925  2gencl  3515  3gencl  3516  vtocl2gf  3560  vtocl3gf  3561  vtocl2g  3562  vtocl3g  3563  vtocl2ga  3566  vtocl4g  3571  eqeu  3701  mo2icl  3709  euind  3719  reu7  3727  reuind  3748  sbctt  3852  reu8nf  3870  sbcnestgfw  4417  sbcnestgf  4422  r19.36zv  4505  dedth2h  4586  dedth3h  4587  dedth4h  4588  reusngf  4675  reuprg0  4705  preq12bg  4853  elint  4955  elintrabg  4964  intab  4981  axrep1  5285  axreplem  5286  axrep2  5287  axrep6g  5292  bm1.3ii  5301  reusv3  5402  poclOLD  5595  swopolem  5597  solin  5612  freq1  5645  frminex  5655  vtoclr  5738  2optocl  5770  3optocl  5771  raliunxp  5838  resieq  5991  iss  6034  cnveqb  6194  reu3op  6290  reuop  6291  dfpo2  6294  preddowncl  6332  funmoOLD  6563  funimaexgOLD  6634  fnbrfvb  6943  fvelimab  6963  fvmptss  7009  fmptco  7128  fprg  7154  fnressn  7157  fressnfv  7159  isoselem  7340  ovg  7574  caovcan  7613  caovordig  7614  caovord  7620  tfisi  7850  tfindsg  7852  tfinds2  7855  tfinds3  7856  dfom2  7859  elom  7860  findsg  7892  finds2  7893  f1o2ndf1  8110  poxp  8116  fnse  8121  xpord3inddlem  8142  soseq  8147  fpr3g  8272  frrlem12  8284  fpr2a  8289  wfr3g  8309  wfrlem4OLD  8314  smoeq  8352  smores  8354  smogt  8369  tfrlem1  8378  tfr3  8401  oaordi  8548  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  8686  2ecoptocl  8804  3ecoptocl  8805  undifixp  8930  xpdom2g  9070  findcard2  9166  unfi  9174  ssfi  9175  imafi  9177  fnfi  9183  findcard2OLD  9286  xpfiOLD  9320  fodomfi  9327  finsschain  9361  marypha1lem  9430  marypha1  9431  supeq1  9442  ordiso2  9512  ordtypelem7  9521  wemaplem1  9543  inf3lem2  9626  inf3lem5  9629  infdiffi  9655  cantnfval2  9666  cantnfle  9668  cantnfp1lem3  9677  oemapval  9680  cantnflem1  9686  cantnf  9690  wemapwe  9694  cnfcom  9697  cnfcom3clem  9702  ttrclss  9717  ttrclselem2  9723  tz9.1  9726  frr3g  9753  frr2  9757  r1pwALT  9843  cplem2  9887  karden  9892  updjud  9931  infxpenc2lem2  10017  fseqenlem1  10021  dfac8clem  10029  alephinit  10092  dfac4  10119  dfac5lem5  10124  dfac2a  10126  dfac2b  10127  dfacacn  10138  dfac12lem3  10142  kmlem2  10148  kmlem13  10159  nnadju  10194  ackbij1lem16  10232  sornom  10274  infpssrlem4  10303  fin23lem14  10330  fin23lem32  10341  fin23lem34  10343  fin23lem36  10345  isf32lem1  10350  isf32lem2  10351  axcc2lem  10433  axcc3  10435  axcclem  10454  zornn0g  10502  ttukeylem5  10510  ttukeylem6  10511  axrepnd  10591  axpowndlem3  10596  zfcndrep  10611  fpwwe2lem7  10634  pwfseqlem3  10657  wunr1om  10716  wunfi  10718  tskr1om  10764  ingru  10812  grudomon  10814  axgroth3  10828  axgroth4  10829  nqereu  10926  mulcanenq  10957  elnp  10984  elnpi  10985  prlem934  11030  infm3  12177  nnindd  12236  nnaddcl  12239  nnmulcl  12240  nnne0  12250  peano5uzi  12655  uzind2  12659  nn0indd  12663  zindd  12667  fzindd  12668  eluzaddOLD  12861  uzaddcl  12892  uzwo  12899  indstr  12904  zmax  12933  xmulasslem  13268  xrsupsslem  13290  xrinfmsslem  13291  xrsupss  13292  xrinfmss  13293  flval2  13783  om2uzlti  13919  uzrdgfni  13927  rabssnn0fi  13955  mptnn0fsupp  13966  seqcl2  13990  seqfveq2  13994  seqshft2  13998  monoord  14002  seqsplit  14005  seqcaopr3  14007  seqf1olem2a  14010  seqf1o  14013  seqid2  14018  seqhomo  14019  ser1const  14028  expcllem  14042  expeq0  14062  mulexp  14071  expadd  14074  expmul  14077  expmordi  14136  leexp2r  14143  leexp1a  14144  bernneq  14196  modexp  14205  facdiv  14251  faclbnd  14254  faclbnd4lem4  14260  hashgadd  14341  hashxp  14398  hashmap  14399  hashf1lem2  14421  hashf1  14422  seqcoll  14429  wrdind  14676  wrd2ind  14677  pfxccatin12lem3  14686  cshweqrep  14775  2cshwcshw  14780  relexp0g  14973  relexpsucnnr  14976  relexpsucnnl  14981  relexpcnv  14986  relexpnndm  14992  relexpaddnn  15002  rtrclreclem1  15008  dfrtrclrec2  15009  rtrclreclem2  15010  rtrclreclem4  15012  dfrtrcl2  15013  relexpind  15015  reusq0  15413  rlim  15443  rlim2  15444  rlim0  15456  rlim0lt  15457  rlimi  15461  ello12r  15465  ello1mpt  15469  ello1d  15471  elo12r  15476  lo1o1  15480  o1lo1  15485  lo1res  15507  climshft  15524  o1compt  15535  rlimo1  15565  lo1add  15575  lo1mul  15576  rlimdiv  15596  climub  15612  climserle  15613  caucvgrlem  15623  caurcvgr  15624  iseraltlem2  15633  summolem2a  15665  sumss  15674  fsum2d  15721  fsumabs  15751  fsumrlim  15761  fsumo1  15762  fsumiun  15771  binom  15780  climcndslem1  15799  climcndslem2  15800  cvgrat  15833  clim2prod  15838  prodfn0  15844  prodfrec  15845  ntrivcvgfvn0  15849  prodmolem2a  15882  fprodabs  15922  fprodn0  15927  fprod2d  15929  binomfallfac  15989  bpolycl  16000  bpolydif  16003  fprodefsum  16042  demoivreALT  16148  ruclem8  16184  ruclem9  16185  dvdsle  16257  dvdsfac  16273  divalglem7  16346  bitsinv1  16387  sadcadd  16403  sadadd2  16405  saddisjlem  16409  smuval2  16427  smupvallem  16428  smu01lem  16430  smupval  16433  smueqlem  16435  smumullem  16437  bezoutlem4  16488  dfgcd2  16492  rplpwr  16503  nn0seqcvgd  16511  seq1st  16512  alginv  16516  algcvga  16520  algfx  16521  lcmf  16574  prmind2  16626  prmdvdsexp  16656  prmfac1  16662  reumodprminv  16741  pcmpt  16829  pcfac  16836  prmpwdvds  16841  prmreclem4  16856  vdwlem10  16927  ramval  16945  ramcl  16966  cshwrepswhash1  17040  prmlem1a  17044  imasleval  17491  ismre  17538  mreexexd  17596  lubprop  18315  lublecllem  18317  glbprop  18328  joinlem  18340  meetlem  18354  poslubmo  18368  posglbmo  18369  poslubd  18370  isglbd  18466  lubun  18472  mndind  18745  frmdgsum  18779  mulgnnass  19025  mhmmulg  19031  gsumwrev  19274  gsmsymgrfix  19337  gsmsymgreq  19341  psgnunilem3  19405  sylow1lem1  19507  efginvrel2  19636  efgsrel  19643  efgredlemd  19653  efgredlem  19656  efgred  19657  efgrelexlemb  19659  gsum2dlem2  19880  gsumcom2  19884  ablfac1eulem  19983  pgpfac1lem2  19986  pgpfac1lem5  19990  pgpfac1  19991  pgpfac  19995  srgmulgass  20111  srgpcomp  20112  srgbinom  20125  lmodvsmmulgdi  20651  isdomn2  21115  cnfldexp  21178  islindf4  21612  assamulgscm  21674  mplcoe1  21811  mplcoe3  21812  mplcoe5  21814  gsummoncoe1  22048  dmatval  22214  dmatel  22215  dmatmulcl  22222  pmatcoe1fsupp  22423  decpmataa0  22490  decpmatmulsumfsupp  22495  pmatcollpw2lem  22499  pm2mpmhmlem1  22540  fiinopn  22623  mretopd  22816  neiptoptop  22855  cnpfval  22958  iscnp3  22968  tgcn  22976  lmbr  22982  lmbr2  22983  lmbrf  22984  lmss  23022  ishaus  23046  hausnei2  23077  t1sep2  23093  fiuncmp  23128  dfconn2  23143  1stcfb  23169  2ndc1stc  23175  1stcrest  23177  1stcelcls  23185  1stccn  23187  lly1stc  23220  elkgen  23260  kgencn  23280  tx1stc  23374  xkopt  23379  cnmptcom  23402  isr0  23461  r0sep  23472  ptcmpfi  23537  isfildlem  23581  rnelfm  23677  fbflim  23700  flimrest  23707  isflf  23717  flffbas  23719  lmflf  23729  fclsrest  23748  isfcf  23758  cnextfvval  23789  tmdgsum  23819  eltsms  23857  tsmsi  23858  tsmsgsum  23863  tsmssubm  23867  tsmsres  23868  tsmsf1o  23869  isust  23928  isucn  24003  isucn2  24004  ucnima  24006  imasdsf1olem  24099  metss  24237  met1stc  24250  metcnp  24270  metcnpi  24273  metcnpi2  24274  metucn  24300  xrge0tsms  24570  fsumcn  24608  elcncf  24629  cncfi  24634  rescncf  24637  cncfco  24647  caucfil  25031  equivcau  25048  caubl  25056  caublcls  25057  ovolgelb  25229  ovolunlem1a  25245  ovolicc2lem3  25268  voliunlem1  25299  voliunlem3  25301  volsuplem  25304  volsup  25305  dyadmax  25347  vitali  25362  itg2leub  25484  itgfsum  25576  dvnadd  25679  dvnres  25681  cpnord  25685  dvnfre  25704  dvmptfsum  25727  dvferm1  25737  dvferm2  25739  rolle  25742  dvlip  25745  c1lip1  25749  lhop1  25766  deg1leb  25848  ply1divex  25889  fta1g  25920  plyco  25990  dgrcolem1  26023  dgrco  26025  dvnply2  26036  plydivex  26046  aalioulem2  26082  aalioulem3  26083  aalioulem5  26085  aaliou3lem2  26092  dvntaylp  26119  taylthlem1  26121  ulmdvlem3  26150  abelthlem9  26188  cxpmul2  26433  scvxcvx  26726  jensenlem2  26728  jensen  26729  wilthlem3  26810  perfectlem2  26969  bcmono  27016  bposlem5  27027  lgsquad2lem2  27124  addsq2reu  27179  2sqreulem1  27185  2sqreunnlem1  27188  dchrisumlem1  27228  dchrisum0flb  27249  pntpbnd1  27325  pntlemf  27344  qabvle  27364  qabvexp  27365  ostthlem2  27367  ostth2lem2  27373  nosupcbv  27441  nosupno  27442  nosupdm  27443  nosupfv  27445  nosupres  27446  nosupbnd1lem1  27447  nosupbnd1lem3  27449  nosupbnd1lem5  27451  noinfcbv  27456  noinfno  27457  noinfdm  27458  noinffv  27460  noinfres  27461  noinfbnd1lem3  27464  noinfbnd1lem5  27466  eqscut2  27544  addsproplem1  27691  addsprop  27698  negsunif  27768  mulsproplem9  27819  ssltmul2  27842  precsexlem8  27899  precsexlem9  27900  precsexlem11  27902  tgcgr4  28049  usgr2pth  29288  wlkiswwlks2lem4  29393  wlkiswwlks2  29396  rusgrnumwwlk  29496  clwlkclwwlklem2a  29518  clwlkclwwlklem1  29519  clwlkclwwlkfo  29529  eupth2  29759  frgr3vlem1  29793  3vfriswmgrlem  29797  3vfriswmgr  29798  wlkl0  29887  numclwlk2lem2f1o  29899  isplig  29996  isnvlem  30130  nvi  30134  nmoubi  30292  nmounbi  30296  nmblolbi  30320  ipasslem1  30351  ipassi  30361  hlim2  30712  pjhth  30913  spansni  31077  elspansn2  31087  pjige0  31211  pjcjt2  31212  pjopyth  31240  elcnop  31377  elcnfn  31402  nmopub  31428  cnopc  31433  nmfnleub  31445  elnlfn  31448  cnfnc  31450  nmbdoplb  31545  nmcexi  31546  nmcoplb  31550  lnfnmul  31568  nmbdfnlb  31570  nmcfnlb  31574  pjss2coi  31684  pjssmi  31685  isst  31733  ishst  31734  stcltr1i  31794  mdbr  31814  dmdbr  31819  mddmd2  31829  mdslmd1lem3  31847  mdslmd1lem4  31848  elat2  31860  atcvat2  31909  cdj1i  31953  iuninc  32059  fmptcof2  32149  nn0min  32293  wrdt2ind  32384  ismnt  32420  xrge0tsmsd  32479  isomnd  32489  omndadd  32494  cyc3genpm  32581  isarchi2  32601  archirng  32604  archiexdiv  32606  archiabl  32614  isorng  32687  ofldchr  32702  islbs5  32770  mxidlval  32851  crefeq  33123  nexple  33305  esumfzf  33365  issiga  33408  isrnsiga  33409  isldsys  33452  ismeas  33495  isrnmeas  33496  measiun  33514  eulerpartlemn  33678  sseqp1  33692  rrvsum  33751  signsply0  33860  signstfvc  33883  bnj941  34081  bnj106  34177  bnj155  34188  bnj590  34219  bnj591  34220  bnj849  34234  bnj893  34237  bnj944  34247  bnj1128  34299  subfacp1lem6  34474  erdszelem8  34487  issconn  34515  cvmliftlem7  34580  cvmliftlem10  34583  cvmlift3lem2  34609  satfsschain  34653  satfrel  34656  satfdm  34658  satfrnmapom  34659  fmlafvel  34674  satffun  34698  mrsubvrs  34811  mclsssvlem  34851  mclsval  34852  mclsax  34858  mclsind  34859  shftvalg  35005  bccolsum  35013  iprodefisumlem  35014  faclimlem1  35017  rdgprc  35070  fveleq  35639  unblimceq0  35686  bj-ax12  35837  bj-bm1.3ii  36248  rdgeqoa  36554  finxpreclem6  36580  domalom  36588  ralssiun  36591  wl-sblimt  36719  wl-sbhbt  36722  wl-2sb6d  36726  wl-mo2df  36738  wl-mo2t  36743  poimirlem2  36793  poimirlem25  36816  poimirlem28  36819  poimirlem31  36822  heicant  36826  mbfresfi  36837  itg2gt0cn  36846  sdclem2  36913  fdc  36916  seqpo  36918  incsequz  36919  mettrifi  36928  prdsbnd2  36966  heiborlem4  36985  bfplem1  36993  iscringd  37169  maxidlval  37210  igenval2  37237  iss2  37516  elrefrels3  37692  ax12eq  38114  ax12el  38115  ax12indalem  38118  ax12inda2ALT  38119  ax12inda  38121  ax12v2-o  38122  riotasvd  38129  isopos  38353  isat3  38480  ishlat1  38525  glbconN  38550  glbconNOLD  38551  ispsubsp  38919  isldil  39284  isltrn  39293  isdilN  39328  trlval  39336  cdleme27b  39542  cdleme29b  39549  cdleme31sn1  39555  cdleme31sn1c  39562  cdleme40v  39643  cdlemk36  40087  cdlemkid5  40109  cdlemn11pre  40384  dihord2pre  40399  islpolN  40657  hdmapffval  41000  hdmapfval  41001  hdmapval2lem  41005  uzindd  41148  sticksstones1  41268  sticksstones2  41269  sticksstones3  41270  sticksstones8  41275  sticksstones10  41277  sticksstones11  41278  sticksstones12a  41279  sticksstones15  41283  nnaddcom  41484  nnadddir  41486  nnmulcom  41488  ismrc  41741  incssnn0  41751  mzpexpmpt  41785  pell14qrexpclnn0  41906  monotuz  41982  rmxypos  41988  jm2.17a  42001  jm2.17b  42002  rmygeid  42005  jm2.18  42029  jm2.19lem3  42032  jm2.25  42040  jm2.15nn0  42044  jm2.16nn0  42045  wepwsolem  42086  aomclem8  42105  dfac11  42106  pwslnm  42138  lnr2i  42160  hbtlem5  42172  cnsrexpcl  42209  rngunsnply  42217  isdomn3  42248  unielss  42269  onsucf1lem  42321  cantnfresb  42376  onmcl  42383  naddonnn  42448  elmapintrab  42629  elmapintab  42649  cnvcnvintabd  42653  eliunov2  42732  relexpxpnnidm  42756  relexpiidm  42757  relexpss1d  42758  iunrelexpmin1  42761  relexpmulnn  42762  iunrelexpmin2  42765  relexp0a  42769  trclimalb2  42779  clsk3nimkb  43093  ntrclsiso  43120  ntrclskb  43122  ntrneiiso  43144  ntrneix2  43146  ntrneixb  43148  gneispace2  43185  gneispacess2  43199  mnuunid  43338  dvgrat  43373  pm14.122b  43484  fnchoice  44015  fiiuncl  44053  ssinc  44077  ssdec  44078  wessf1ornlem  44182  dmrelrnrel  44223  fperiodmullem  44311  monoordxrv  44490  fmul01  44594  fmuldfeq  44597  climsuselem1  44621  climinff  44625  ellimcabssub0  44631  limcleqr  44658  addlimc  44662  0ellimcdiv  44663  limclner  44665  limsupref  44699  limsupub  44718  limsupmnf  44735  limsupre2lem  44738  limsupre2  44739  limsupre2mpt  44744  limsupre3lem  44746  limsupre3  44747  limsupre3mpt  44748  xlimbr  44841  cnrefiisplem  44843  dvnmptdivc  44952  dvnmptconst  44955  dvnmul  44957  iblspltprt  44987  itgspltprt  44993  stoweidlem2  45016  stoweidlem3  45017  stoweidlem17  45031  stoweidlem19  45033  stoweidlem21  45035  stoweidlem26  45040  fourierdlem42  45163  issal  45328  ismea  45465  isome  45508  carageniuncllem1  45535  caratheodorylem1  45540  2reu8i  46119  2reuimp0  46120  funressndmafv2rn  46229  2ffzoeq  46334  smonoord  46337  fargshiftf1  46407  ichnfimlem  46429  paireqne  46477  reupr  46488  reuopreuprim  46492  perfectALTVlem2  46688  lmodvsmdi  47146  dmatALTval  47168  dmatALTbasel  47170  snlindsntor  47239  ldepsnlinc  47276  elbigo2r  47326  elbigolo1  47330  itcovalt2  47450  mof0  47591  isnrm4  47650  iscnrm3r  47668  iscnrm4  47674  lubsscl  47680  glbsscl  47681  ipolubdm  47699  ipoglbdm  47702  setrecseq  47817  setrec2fun  47824  setrec2lem2  47826