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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced 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  9872  karden  9877  updjud  9916  infxpenc2lem2  10000  fseqenlem1  10004  dfac8clem  10012  alephinit  10075  dfac4  10102  dfac5lem5  10107  dfac2a  10109  dfac2b  10110  dfacacn  10121  dfac12lem3  10125  kmlem2  10131  kmlem13  10142  nnadju  10177  ackbij1lem16  10213  sornom  10256  infpssrlem4  10285  fin23lem14  10312  fin23lem32  10323  fin23lem34  10325  fin23lem36  10327  isf32lem1  10332  isf32lem2  10333  axcc2lem  10415  axcc3  10417  axcclem  10436  zornn0g  10484  ttukeylem5  10492  ttukeylem6  10493  axrepnd  10574  axpowndlem3  10579  zfcndrep  10594  fpwwe2lem7  10617  pwfseqlem3  10640  wunr1om  10699  wunfi  10701  tskr1om  10747  ingru  10795  grudomon  10797  axgroth3  10811  axgroth4  10812  nqereu  10909  mulcanenq  10940  elnp  10967  elnpi  10968  prlem934  11013  infm3  12169  nnindd  12248  nnaddcl  12251  nnmulcl  12252  nnaddcom  12255  nnne0  12265  nnadddir  12287  nnmulcom  12289  peano5uzi  12680  uzind2  12684  nn0indd  12688  zindd  12692  fzindd  12693  uzaddcl  12923  uzwo  12930  indstr  12935  zmax  12964  xmulasslem  13306  xrsupsslem  13328  xrinfmsslem  13329  xrsupss  13330  xrinfmss  13331  flval2  13843  om2uzlti  13982  uzrdgfni  13990  rabssnn0fi  14018  mptnn0fsupp  14029  seqcl2  14052  seqfveq2  14056  seqshft2  14060  monoord  14064  seqsplit  14067  seqcaopr3  14069  seqf1olem2a  14072  seqf1o  14075  seqid2  14080  seqhomo  14081  ser1const  14090  expcllem  14104  expeq0  14124  mulexp  14133  expadd  14136  expmul  14139  expmordi  14199  leexp2r  14206  leexp1a  14207  bernneq  14261  modexp  14270  facdiv  14319  faclbnd  14322  faclbnd4lem4  14328  hashgadd  14409  hashxp  14467  hashmap  14468  hashf1lem2  14489  hashf1  14490  seqcoll  14497  wrdind  14755  wrd2ind  14756  pfxccatin12lem3  14765  cshweqrep  14854  2cshwcshw  14858  relexp0g  15055  relexpsucnnr  15058  relexpsucnnl  15063  relexpcnv  15068  relexpnndm  15074  relexpaddnn  15084  rtrclreclem1  15090  dfrtrclrec2  15091  rtrclreclem2  15092  rtrclreclem4  15094  dfrtrcl2  15095  relexpind  15097  reusq0  15512  rlim  15542  rlim2  15543  rlim0  15555  rlim0lt  15556  rlimi  15560  ello12r  15564  ello1mpt  15568  ello1d  15570  elo12r  15575  lo1o1  15579  o1lo1  15584  lo1res  15606  climshft  15623  o1compt  15634  rlimo1  15664  lo1add  15674  lo1mul  15675  rlimdiv  15693  climub  15709  climserle  15710  caucvgrlem  15720  caurcvgr  15721  iseraltlem2  15730  summolem2a  15762  sumss  15771  fsum2d  15818  fsumabs  15849  fsumrlim  15859  fsumo1  15860  fsumiun  15869  binom  15880  climcndslem1  15899  climcndslem2  15900  cvgrat  15933  clim2prod  15938  prodfn0  15944  prodfrec  15945  ntrivcvgfvn0  15949  prodmolem2a  15984  fprodabs  16024  fprodn0  16029  fprod2d  16031  binomfallfac  16090  bpolycl  16101  bpolydif  16104  fprodefsum  16144  demoivreALT  16252  ruclem8  16288  ruclem9  16289  dvdsle  16363  dvdsfac  16379  divalglem7  16452  bitsinv1  16495  sadcadd  16511  sadadd2  16513  saddisjlem  16517  smuval2  16535  smupvallem  16536  smu01lem  16538  smupval  16541  smueqlem  16543  smumullem  16545  bezoutlem4  16595  dfgcd2  16599  rplpwr  16611  nn0seqcvgd  16623  seq1st  16624  alginv  16628  algcvga  16632  algfx  16633  lcmf  16686  prmind2  16738  prmdvdsexp  16769  prmfac1  16774  reumodprminv  16859  pcmpt  16947  pcfac  16954  prmpwdvds  16959  prmreclem4  16974  vdwlem10  17045  ramval  17063  ramcl  17084  cshwrepswhash1  17157  prmlem1a  17161  imasleval  17590  ismre  17637  mreexexd  17699  lubprop  18407  lublecllem  18409  glbprop  18420  joinlem  18432  meetlem  18446  poslubmo  18460  posglbmo  18461  poslubd  18462  isglbd  18560  lubun  18566  mndind  18882  frmdgsum  18916  mulgnnass  19170  mhmmulg  19176  gsumwrev  19431  gsmsymgrfix  19493  gsmsymgreq  19497  psgnunilem3  19561  sylow1lem1  19663  efginvrel2  19792  efgsrel  19799  efgredlemd  19809  efgredlem  19812  efgred  19813  efgrelexlemb  19815  gsum2dlem2  20036  gsumcom2  20040  ablfac1eulem  20139  pgpfac1lem2  20142  pgpfac1lem5  20146  pgpfac1  20147  pgpfac  20151  isomnd  20188  omndadd  20193  srgmulgass  20294  srgpcomp  20295  srgbinom  20308  isdomn3  20813  isorng  20964  lmodvsmmulgdi  21018  rspprop  21370  cnfldexp  21555  ofldchr  21726  islindf4  21988  assamulgscm  22051  mplcoe1  22188  mplcoe3  22189  mplcoe5  22191  gsummoncoe1  22468  dmatval  22649  dmatel  22650  dmatmulcl  22657  pmatcoe1fsupp  22858  decpmataa0  22925  decpmatmulsumfsupp  22930  pmatcollpw2lem  22934  pm2mpmhmlem1  22975  fiinopn  23058  mretopd  23249  neiptoptop  23288  cnpfval  23391  iscnp3  23401  tgcn  23409  lmbr  23415  lmbr2  23416  lmbrf  23417  lmss  23455  ishaus  23479  hausnei2  23510  t1sep2  23526  fiuncmp  23561  dfconn2  23576  1stcfb  23602  2ndc1stc  23608  1stcrest  23610  1stcelcls  23618  1stccn  23620  lly1stc  23653  elkgen  23693  kgencn  23713  tx1stc  23807  xkopt  23812  cnmptcom  23835  isr0  23894  r0sep  23905  ptcmpfi  23970  isfildlem  24014  rnelfm  24110  fbflim  24133  flimrest  24140  isflf  24150  flffbas  24152  lmflf  24162  fclsrest  24181  isfcf  24191  cnextfvval  24222  tmdgsum  24252  eltsms  24290  tsmsi  24291  tsmsgsum  24296  tsmssubm  24300  tsmsres  24301  tsmsf1o  24302  isust  24361  isucn  24434  isucn2  24435  ucnima  24437  imasdsf1olem  24530  metss  24665  met1stc  24678  metcnp  24698  metcnpi  24701  metcnpi2  24702  metucn  24728  xrge0tsms  24992  fsumcn  25029  elcncf  25048  cncfi  25053  rescncf  25056  cncfco  25066  caucfil  25442  equivcau  25459  caubl  25467  caublcls  25468  ovolgelb  25639  ovolunlem1a  25655  ovolicc2lem3  25678  voliunlem1  25709  voliunlem3  25711  volsuplem  25714  volsup  25715  dyadmax  25757  vitali  25772  itg2leub  25893  itgfsum  25986  dvnadd  26088  dvnres  26090  cpnord  26094  dvnfre  26111  dvmptfsum  26134  dvferm1  26144  dvferm2  26146  rolle  26149  dvlip  26152  c1lip1  26156  lhop1  26173  deg1leb  26252  ply1divex  26294  fta1g  26327  plyco  26398  dgrcolem1  26430  dgrco  26432  dvnply2  26448  plydivex  26458  aalioulem2  26496  aalioulem3  26497  aalioulem5  26499  aaliou3lem2  26506  dvntaylp  26534  taylthlem1  26536  ulmdvlem3  26565  abelthlem9  26603  cxpmul2  26854  scvxcvx  27150  jensenlem2  27152  jensen  27153  wilthlem3  27234  perfectlem2  27394  bcmono  27441  bposlem5  27452  lgsquad2lem2  27549  addsq2reu  27604  2sqreulem1  27610  2sqreunnlem1  27613  dchrisumlem1  27653  dchrisum0flb  27674  pntpbnd1  27750  pntlemf  27769  qabvle  27789  qabvexp  27790  ostthlem2  27792  ostth2lem2  27798  nosupcbv  27866  nosupno  27867  nosupdm  27868  nosupfv  27870  nosupres  27871  nosupbnd1lem1  27872  nosupbnd1lem3  27874  nosupbnd1lem5  27876  noinfcbv  27881  noinfno  27882  noinfdm  27883  noinffv  27885  noinfres  27886  noinfbnd1lem3  27889  noinfbnd1lem5  27891  eqcuts2  27979  addsproplem1  28162  addsprop  28169  negsunif  28248  mulsproplem9  28317  sltmuls2  28341  precsexlem8  28407  precsexlem9  28408  precsexlem11  28410  noseqind  28485  om2noseqrdg  28497  noseqrdgfn  28499  n0addscl  28537  n0mulscl  28538  eucliddivs  28569  peano5uzs  28597  expscllem  28623  expadds  28628  expsne0  28629  expsgt0  28630  pw2cut  28653  pw2cut2  28655  bdaypw2n0bnd  28657  tgcgr4  28800  prlngmo2  29206  usgr2pth  30113  wlkiswwlks2lem4  30221  wlkiswwlks2  30224  rusgrnumwwlk  30327  clwlkclwwlklem2a  30349  clwlkclwwlklem1  30350  clwlkclwwlkfo  30360  eupth2  30590  frgr3vlem1  30624  3vfriswmgrlem  30628  3vfriswmgr  30629  wlkl0  30718  numclwlk2lem2f1o  30730  isplig  30828  isnvlem  30962  nvi  30966  nmoubi  31124  nmounbi  31128  nmblolbi  31152  ipasslem1  31183  ipassi  31193  hlim2  31544  pjhth  31745  spansni  31909  elspansn2  31919  pjige0  32043  pjcjt2  32044  pjopyth  32072  elcnop  32209  elcnfn  32234  nmopub  32260  cnopc  32265  nmfnleub  32277  elnlfn  32280  cnfnc  32282  nmbdoplb  32377  nmcexi  32378  nmcoplb  32382  lnfnmul  32400  nmbdfnlb  32402  nmcfnlb  32406  pjss2coi  32516  pjssmi  32517  isst  32565  ishst  32566  stcltr1i  32626  mdbr  32646  dmdbr  32651  mddmd2  32661  mdslmd1lem3  32679  mdslmd1lem4  32680  elat2  32692  atcvat2  32741  cdj1i  32785  iuninc  32905  fmptcof2  33002  nn0min  33165  nexple  33177  wrdt2ind  33273  ismnt  33303  xrge0tsmsd  33393  gsumwun  33396  cyc3genpm  33472  isarchi2  33505  archirng  33508  archiexdiv  33510  archiabl  33518  domnprodn0  33598  islbs5  33693  unitprodclb  33702  mxidlval  33744  1arithidom  33827  1arithufdlem3  33836  crefeq  34235  esumfzf  34459  issiga  34502  isrnsiga  34503  isldsys  34546  ismeas  34589  isrnmeas  34590  measiun  34608  eulerpartlemn  34771  sseqp1  34785  rrvsum  34844  signsply0  34938  signstfvc  34961  bnj941  35161  bnj106  35256  bnj155  35267  bnj590  35298  bnj591  35299  bnj849  35313  bnj893  35316  bnj944  35326  bnj1128  35378  r1filimi  35497  r1omhfb  35508  tz9.1regs  35547  r1omhfbregs  35550  elkarden  35568  gblacfnacd  35586  subfacp1lem6  35677  erdszelem8  35690  issconn  35718  cvmliftlem7  35783  cvmliftlem10  35786  cvmlift3lem2  35812  satfsschain  35856  satfrel  35859  satfdm  35861  satfrnmapom  35862  fmlafvel  35877  satffun  35901  mrsubvrs  36014  mclsssvlem  36054  mclsval  36055  mclsax  36061  mclsind  36062  shftvalg  36224  bccolsum  36231  iprodefisumlem  36232  faclimlem1  36235  rdgprc  36284  nmuladdss  36690  sbequbidv  36726  cbvsbdavw  36766  fveleq  36962  dfttc4lem1  37039  dfttc4  37041  elttcirr  37042  regsfromregtco  37049  mh-unprimbi  37055  unblimceq0  37096  bj-ax12  37279  bj-bm1.3ii  37700  rdgeqoa  38016  finxpreclem6  38042  domalom  38050  ralssiun  38053  wl-ax12v2cl  38152  wl-sblimt  38203  wl-sbhbt  38209  wl-2sb6d  38213  wl-mo2df  38225  wl-mo2t  38230  poimirlem2  38273  poimirlem25  38296  poimirlem28  38299  poimirlem31  38302  heicant  38306  mbfresfi  38317  itg2gt0cn  38326  sdclem2  38393  fdc  38396  seqpo  38398  incsequz  38399  mettrifi  38408  prdsbnd2  38446  heiborlem4  38465  bfplem1  38473  iscringd  38649  maxidlval  38690  igenval2  38717  iss2  38993  elrefrels3  39248  ax12eq  39715  ax12el  39716  ax12indalem  39719  ax12inda2ALT  39720  ax12inda  39722  ax12v2-o  39723  riotasvd  39730  isopos  39954  isat3  40081  ishlat1  40126  glbconN  40151  ispsubsp  40519  isldil  40884  isltrn  40893  isdilN  40928  trlval  40936  cdleme27b  41142  cdleme29b  41149  cdleme31sn1  41155  cdleme31sn1c  41162  cdleme40v  41243  cdlemk36  41687  cdlemkid5  41709  cdlemn11pre  41984  dihord2pre  41999  islpolN  42257  hdmapffval  42600  hdmapfval  42601  hdmapval2lem  42605  uzindd  42745  sticksstones1  42913  sticksstones2  42914  sticksstones3  42915  sticksstones8  42920  sticksstones10  42922  sticksstones11  42923  sticksstones12a  42924  sticksstones15  42928  indstrd  42960  unitscyglem3  42964  eu6w  43408  ismrc  43432  incssnn0  43442  mzpexpmpt  43476  pell14qrexpclnn0  43593  monotuz  43668  rmxypos  43674  jm2.17a  43687  jm2.17b  43688  rmygeid  43691  jm2.18  43715  jm2.19lem3  43718  jm2.25  43726  jm2.15nn0  43730  jm2.16nn0  43731  wepwsolem  43769  aomclem8  43788  dfac11  43789  pwslnm  43821  lnr2i  43843  hbtlem5  43855  cnsrexpcl  43892  rngunsnply  43896  unielss  43945  onsucf1lem  43996  cantnfresb  44051  onmcl  44058  naddonnn  44122  elmapintrab  44302  elmapintab  44322  cnvcnvintabd  44326  eliunov2  44405  relexpxpnnidm  44429  relexpiidm  44430  relexpss1d  44431  iunrelexpmin1  44434  relexpmulnn  44435  iunrelexpmin2  44438  relexp0a  44442  trclimalb2  44452  clsk3nimkb  44766  ntrclsiso  44793  ntrclskb  44795  ntrneiiso  44817  ntrneix2  44819  ntrneixb  44821  gneispace2  44858  gneispacess2  44872  mnuunid  44987  dvgrat  45022  pm14.122b  45133  relpeq1  45653  relpeq3  45655  trfr  45671  pwclaxpow  45693  prclaxpr  45694  uniclaxun  45695  modelac8prim  45701  permaxpow  45718  permaxpr  45719  permaxun  45720  nregmodel  45726  fnchoice  45749  fiiuncl  45785  ssinc  45805  ssdec  45806  wessf1ornlem  45903  dmrelrnrel  45942  fperiodmullem  46022  monoordxrv  46195  fmul01  46296  fmuldfeq  46299  climsuselem1  46323  climinff  46327  ellimcabssub0  46333  limcleqr  46358  addlimc  46362  0ellimcdiv  46363  limclner  46365  limsupref  46399  limsupub  46418  limsupmnf  46435  limsupre2lem  46438  limsupre2  46439  limsupre2mpt  46444  limsupre3lem  46446  limsupre3  46447  limsupre3mpt  46448  xlimbr  46541  cnrefiisplem  46543  dvnmptdivc  46652  dvnmptconst  46655  dvnmul  46657  iblspltprt  46687  itgspltprt  46693  stoweidlem2  46716  stoweidlem3  46717  stoweidlem17  46731  stoweidlem19  46733  stoweidlem21  46735  stoweidlem26  46740  fourierdlem42  46863  issal  47028  ismea  47165  isome  47208  carageniuncllem1  47235  caratheodorylem1  47240  2reu8i  47850  2reuimp0  47851  funressndmafv2rn  47960  2ffzoeq  48065  smonoord  48114  fargshiftf1  48190  ichnfimlem  48212  paireqne  48260  reupr  48271  reuopreuprim  48275  perfectALTVlem2  48487  grimcnv  48653  pgnbgreunbgrlem1  48878  pgnbgreunbgrlem4  48884  pgnbgreunbgr  48890  lmodvsmdi  49159  dmatALTval  49180  dmatALTbasel  49182  snlindsntor  49251  ldepsnlinc  49288  elbigo2r  49333  elbigolo1  49337  itcovalt2  49457  mof0  49616  isnrm4  49709  iscnrm3r  49726  iscnrm4  49732  lubsscl  49738  glbsscl  49739  ipolubdm  49765  ipoglbdm  49768  setrecseq  50463  setrec2fun  50470  setrec2lem2  50472