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  913  19.23t  2198  axc14  2456  mojust  2527  mof  2551  eu6lem  2561  nfabdwOLD  2916  2gencl  3505  3gencl  3506  vtocl2gf  3551  vtocl3gf  3552  vtocl2g  3553  vtocl3g  3554  vtocl2ga  3557  vtocl2gaf  3558  vtocl3gaf  3560  vtocl3ga  3562  vtocl4g  3565  vtocl4ga  3566  eqeu  3698  mo2icl  3706  euind  3716  reu7  3724  reuind  3745  sbctt  3849  reu8nf  3867  sbcnestgfw  4420  sbcnestgf  4425  r19.36zv  4508  dedth2h  4589  dedth3h  4590  dedth4h  4591  reusngf  4678  reuprg0  4708  preq12bg  4856  elint  4956  elintrabg  4965  intab  4982  axrep1  5287  axreplem  5288  axrep2  5289  axrep6g  5294  bm1.3ii  5303  reusv3  5405  poclOLD  5598  swopolem  5600  solin  5615  freq1  5648  frminex  5658  vtoclr  5741  2optocl  5773  3optocl  5774  raliunxp  5842  resieq  5996  iss  6040  cnveqb  6202  reu3op  6298  reuop  6299  dfpo2  6302  preddowncl  6340  funmoOLD  6570  funimaexgOLD  6641  fnbrfvb  6949  fvelimab  6970  fvmptss  7016  fmptco  7138  fprg  7164  fnressn  7167  fressnfv  7169  isoselem  7348  ovg  7586  caovcan  7625  caovordig  7626  caovord  7632  tfisi  7864  tfindsg  7866  tfinds2  7869  tfinds3  7870  dfom2  7873  elom  7874  findsg  7905  finds2  7906  f1o2ndf1  8127  poxp  8133  fnse  8138  xpord3inddlem  8159  soseq  8164  fpr3g  8291  frrlem12  8303  fpr2a  8308  wfr3g  8328  wfrlem4OLD  8333  smoeq  8371  smores  8373  smogt  8388  tfrlem1  8397  tfr3  8420  oaordi  8567  oeordi  8608  oeoa  8618  oeoe  8620  nnacl  8632  nnmcl  8633  nnecl  8634  nnacom  8638  nnaordi  8639  nnawordi  8642  nnaass  8643  nndi  8644  nnmass  8645  nnmsucr  8646  nnmcom  8647  nnmordi  8652  naddssim  8706  2ecoptocl  8827  3ecoptocl  8828  undifixp  8953  xpdom2g  9093  findcard2  9189  unfi  9197  ssfi  9198  imafi  9200  fnfi  9206  findcard2OLD  9309  xpfiOLD  9344  fodomfi  9351  finsschain  9385  marypha1lem  9458  marypha1  9459  supeq1  9470  ordiso2  9540  ordtypelem7  9549  wemaplem1  9571  inf3lem2  9654  inf3lem5  9657  infdiffi  9683  cantnfval2  9694  cantnfle  9696  cantnfp1lem3  9705  oemapval  9708  cantnflem1  9714  cantnf  9718  wemapwe  9722  cnfcom  9725  cnfcom3clem  9730  ttrclss  9745  ttrclselem2  9751  tz9.1  9754  frr3g  9781  frr2  9785  r1pwALT  9871  cplem2  9915  karden  9920  updjud  9959  infxpenc2lem2  10045  fseqenlem1  10049  dfac8clem  10057  alephinit  10120  dfac4  10147  dfac5lem5  10152  dfac2a  10154  dfac2b  10155  dfacacn  10166  dfac12lem3  10170  kmlem2  10176  kmlem13  10187  nnadju  10222  ackbij1lem16  10260  sornom  10302  infpssrlem4  10331  fin23lem14  10358  fin23lem32  10369  fin23lem34  10371  fin23lem36  10373  isf32lem1  10378  isf32lem2  10379  axcc2lem  10461  axcc3  10463  axcclem  10482  zornn0g  10530  ttukeylem5  10538  ttukeylem6  10539  axrepnd  10619  axpowndlem3  10624  zfcndrep  10639  fpwwe2lem7  10662  pwfseqlem3  10685  wunr1om  10744  wunfi  10746  tskr1om  10792  ingru  10840  grudomon  10842  axgroth3  10856  axgroth4  10857  nqereu  10954  mulcanenq  10985  elnp  11012  elnpi  11013  prlem934  11058  infm3  12206  nnindd  12265  nnaddcl  12268  nnmulcl  12269  nnne0  12279  peano5uzi  12684  uzind2  12688  nn0indd  12692  zindd  12696  fzindd  12697  eluzaddOLD  12890  uzaddcl  12921  uzwo  12928  indstr  12933  zmax  12962  xmulasslem  13299  xrsupsslem  13321  xrinfmsslem  13322  xrsupss  13323  xrinfmss  13324  flval2  13815  om2uzlti  13951  uzrdgfni  13959  rabssnn0fi  13987  mptnn0fsupp  13998  seqcl2  14021  seqfveq2  14025  seqshft2  14029  monoord  14033  seqsplit  14036  seqcaopr3  14038  seqf1olem2a  14041  seqf1o  14044  seqid2  14049  seqhomo  14050  ser1const  14059  expcllem  14073  expeq0  14093  mulexp  14102  expadd  14105  expmul  14108  expmordi  14167  leexp2r  14174  leexp1a  14175  bernneq  14227  modexp  14236  facdiv  14282  faclbnd  14285  faclbnd4lem4  14291  hashgadd  14372  hashxp  14429  hashmap  14430  hashf1lem2  14453  hashf1  14454  seqcoll  14461  wrdind  14708  wrd2ind  14709  pfxccatin12lem3  14718  cshweqrep  14807  2cshwcshw  14812  relexp0g  15005  relexpsucnnr  15008  relexpsucnnl  15013  relexpcnv  15018  relexpnndm  15024  relexpaddnn  15034  rtrclreclem1  15040  dfrtrclrec2  15041  rtrclreclem2  15042  rtrclreclem4  15044  dfrtrcl2  15045  relexpind  15047  reusq0  15445  rlim  15475  rlim2  15476  rlim0  15488  rlim0lt  15489  rlimi  15493  ello12r  15497  ello1mpt  15501  ello1d  15503  elo12r  15508  lo1o1  15512  o1lo1  15517  lo1res  15539  climshft  15556  o1compt  15567  rlimo1  15597  lo1add  15607  lo1mul  15608  rlimdiv  15628  climub  15644  climserle  15645  caucvgrlem  15655  caurcvgr  15656  iseraltlem2  15665  summolem2a  15697  sumss  15706  fsum2d  15753  fsumabs  15783  fsumrlim  15793  fsumo1  15794  fsumiun  15803  binom  15812  climcndslem1  15831  climcndslem2  15832  cvgrat  15865  clim2prod  15870  prodfn0  15876  prodfrec  15877  ntrivcvgfvn0  15881  prodmolem2a  15914  fprodabs  15954  fprodn0  15959  fprod2d  15961  binomfallfac  16021  bpolycl  16032  bpolydif  16035  fprodefsum  16075  demoivreALT  16181  ruclem8  16217  ruclem9  16218  dvdsle  16290  dvdsfac  16306  divalglem7  16379  bitsinv1  16420  sadcadd  16436  sadadd2  16438  saddisjlem  16442  smuval2  16460  smupvallem  16461  smu01lem  16463  smupval  16466  smueqlem  16468  smumullem  16470  bezoutlem4  16521  dfgcd2  16525  rplpwr  16536  nn0seqcvgd  16544  seq1st  16545  alginv  16549  algcvga  16553  algfx  16554  lcmf  16607  prmind2  16659  prmdvdsexp  16689  prmfac1  16695  reumodprminv  16776  pcmpt  16864  pcfac  16871  prmpwdvds  16876  prmreclem4  16891  vdwlem10  16962  ramval  16980  ramcl  17001  cshwrepswhash1  17075  prmlem1a  17079  imasleval  17526  ismre  17573  mreexexd  17631  lubprop  18353  lublecllem  18355  glbprop  18366  joinlem  18378  meetlem  18392  poslubmo  18406  posglbmo  18407  poslubd  18408  isglbd  18504  lubun  18510  mndind  18788  frmdgsum  18822  mulgnnass  19072  mhmmulg  19078  gsumwrev  19332  gsmsymgrfix  19395  gsmsymgreq  19399  psgnunilem3  19463  sylow1lem1  19565  efginvrel2  19694  efgsrel  19701  efgredlemd  19711  efgredlem  19714  efgred  19715  efgrelexlemb  19717  gsum2dlem2  19938  gsumcom2  19942  ablfac1eulem  20041  pgpfac1lem2  20044  pgpfac1lem5  20048  pgpfac1  20049  pgpfac  20053  srgmulgass  20169  srgpcomp  20170  srgbinom  20183  lmodvsmmulgdi  20792  isdomn2  21263  isdomn3  21265  cnfldexp  21349  islindf4  21789  assamulgscm  21851  mplcoe1  21997  mplcoe3  21998  mplcoe5  22000  gsummoncoe1  22252  dmatval  22438  dmatel  22439  dmatmulcl  22446  pmatcoe1fsupp  22647  decpmataa0  22714  decpmatmulsumfsupp  22719  pmatcollpw2lem  22723  pm2mpmhmlem1  22764  fiinopn  22847  mretopd  23040  neiptoptop  23079  cnpfval  23182  iscnp3  23192  tgcn  23200  lmbr  23206  lmbr2  23207  lmbrf  23208  lmss  23246  ishaus  23270  hausnei2  23301  t1sep2  23317  fiuncmp  23352  dfconn2  23367  1stcfb  23393  2ndc1stc  23399  1stcrest  23401  1stcelcls  23409  1stccn  23411  lly1stc  23444  elkgen  23484  kgencn  23504  tx1stc  23598  xkopt  23603  cnmptcom  23626  isr0  23685  r0sep  23696  ptcmpfi  23761  isfildlem  23805  rnelfm  23901  fbflim  23924  flimrest  23931  isflf  23941  flffbas  23943  lmflf  23953  fclsrest  23972  isfcf  23982  cnextfvval  24013  tmdgsum  24043  eltsms  24081  tsmsi  24082  tsmsgsum  24087  tsmssubm  24091  tsmsres  24092  tsmsf1o  24093  isust  24152  isucn  24227  isucn2  24228  ucnima  24230  imasdsf1olem  24323  metss  24461  met1stc  24474  metcnp  24494  metcnpi  24497  metcnpi2  24498  metucn  24524  xrge0tsms  24794  fsumcn  24832  elcncf  24853  cncfi  24858  rescncf  24861  cncfco  24871  caucfil  25255  equivcau  25272  caubl  25280  caublcls  25281  ovolgelb  25453  ovolunlem1a  25469  ovolicc2lem3  25492  voliunlem1  25523  voliunlem3  25525  volsuplem  25528  volsup  25529  dyadmax  25571  vitali  25586  itg2leub  25708  itgfsum  25800  dvnadd  25903  dvnres  25905  cpnord  25909  dvnfre  25928  dvmptfsum  25951  dvferm1  25961  dvferm2  25963  rolle  25966  dvlip  25970  c1lip1  25974  lhop1  25991  deg1leb  26075  ply1divex  26117  fta1g  26149  plyco  26220  dgrcolem1  26253  dgrco  26255  dvnply2  26267  plydivex  26277  aalioulem2  26313  aalioulem3  26314  aalioulem5  26316  aaliou3lem2  26323  dvntaylp  26351  taylthlem1  26353  ulmdvlem3  26383  abelthlem9  26422  cxpmul2  26668  scvxcvx  26963  jensenlem2  26965  jensen  26966  wilthlem3  27047  perfectlem2  27208  bcmono  27255  bposlem5  27266  lgsquad2lem2  27363  addsq2reu  27418  2sqreulem1  27424  2sqreunnlem1  27427  dchrisumlem1  27467  dchrisum0flb  27488  pntpbnd1  27564  pntlemf  27583  qabvle  27603  qabvexp  27604  ostthlem2  27606  ostth2lem2  27612  nosupcbv  27681  nosupno  27682  nosupdm  27683  nosupfv  27685  nosupres  27686  nosupbnd1lem1  27687  nosupbnd1lem3  27689  nosupbnd1lem5  27691  noinfcbv  27696  noinfno  27697  noinfdm  27698  noinffv  27700  noinfres  27701  noinfbnd1lem3  27704  noinfbnd1lem5  27706  eqscut2  27785  addsproplem1  27932  addsprop  27939  negsunif  28013  mulsproplem9  28074  ssltmul2  28098  precsexlem8  28162  precsexlem9  28163  precsexlem11  28165  noseqind  28215  om2noseqrdg  28227  noseqrdgfn  28229  n0addscl  28262  n0mulscl  28263  tgcgr4  28407  usgr2pth  29650  wlkiswwlks2lem4  29755  wlkiswwlks2  29758  rusgrnumwwlk  29858  clwlkclwwlklem2a  29880  clwlkclwwlklem1  29881  clwlkclwwlkfo  29891  eupth2  30121  frgr3vlem1  30155  3vfriswmgrlem  30159  3vfriswmgr  30160  wlkl0  30249  numclwlk2lem2f1o  30261  isplig  30358  isnvlem  30492  nvi  30496  nmoubi  30654  nmounbi  30658  nmblolbi  30682  ipasslem1  30713  ipassi  30723  hlim2  31074  pjhth  31275  spansni  31439  elspansn2  31449  pjige0  31573  pjcjt2  31574  pjopyth  31602  elcnop  31739  elcnfn  31764  nmopub  31790  cnopc  31795  nmfnleub  31807  elnlfn  31810  cnfnc  31812  nmbdoplb  31907  nmcexi  31908  nmcoplb  31912  lnfnmul  31930  nmbdfnlb  31932  nmcfnlb  31936  pjss2coi  32046  pjssmi  32047  isst  32095  ishst  32096  stcltr1i  32156  mdbr  32176  dmdbr  32181  mddmd2  32191  mdslmd1lem3  32209  mdslmd1lem4  32210  elat2  32222  atcvat2  32271  cdj1i  32315  iuninc  32430  fmptcof2  32524  nn0min  32668  wrdt2ind  32763  ismnt  32799  xrge0tsmsd  32861  isomnd  32871  omndadd  32876  cyc3genpm  32965  isarchi2  32985  archirng  32988  archiexdiv  32990  archiabl  32998  domnprodn0  33065  isorng  33113  ofldchr  33128  islbs5  33192  unitprodclb  33201  mxidlval  33273  1arithidom  33349  1arithufdlem3  33361  crefeq  33577  nexple  33759  esumfzf  33819  issiga  33862  isrnsiga  33863  isldsys  33906  ismeas  33949  isrnmeas  33950  measiun  33968  eulerpartlemn  34132  sseqp1  34146  rrvsum  34205  signsply0  34314  signstfvc  34337  bnj941  34534  bnj106  34630  bnj155  34641  bnj590  34672  bnj591  34673  bnj849  34687  bnj893  34690  bnj944  34700  bnj1128  34752  subfacp1lem6  34926  erdszelem8  34939  issconn  34967  cvmliftlem7  35032  cvmliftlem10  35035  cvmlift3lem2  35061  satfsschain  35105  satfrel  35108  satfdm  35110  satfrnmapom  35111  fmlafvel  35126  satffun  35150  mrsubvrs  35263  mclsssvlem  35303  mclsval  35304  mclsax  35310  mclsind  35311  shftvalg  35457  bccolsum  35464  iprodefisumlem  35465  faclimlem1  35468  rdgprc  35521  fveleq  36066  unblimceq0  36113  bj-ax12  36264  bj-bm1.3ii  36674  rdgeqoa  36980  finxpreclem6  37006  domalom  37014  ralssiun  37017  wl-sblimt  37146  wl-sbhbt  37152  wl-2sb6d  37156  wl-mo2df  37168  wl-mo2t  37173  poimirlem2  37226  poimirlem25  37249  poimirlem28  37252  poimirlem31  37255  heicant  37259  mbfresfi  37270  itg2gt0cn  37279  sdclem2  37346  fdc  37349  seqpo  37351  incsequz  37352  mettrifi  37361  prdsbnd2  37399  heiborlem4  37418  bfplem1  37426  iscringd  37602  maxidlval  37643  igenval2  37670  iss2  37946  elrefrels3  38121  ax12eq  38543  ax12el  38544  ax12indalem  38547  ax12inda2ALT  38548  ax12inda  38550  ax12v2-o  38551  riotasvd  38558  isopos  38782  isat3  38909  ishlat1  38954  glbconN  38979  glbconNOLD  38980  ispsubsp  39348  isldil  39713  isltrn  39722  isdilN  39757  trlval  39765  cdleme27b  39971  cdleme29b  39978  cdleme31sn1  39984  cdleme31sn1c  39991  cdleme40v  40072  cdlemk36  40516  cdlemkid5  40538  cdlemn11pre  40813  dihord2pre  40828  islpolN  41086  hdmapffval  41429  hdmapfval  41430  hdmapval2lem  41434  uzindd  41579  sticksstones1  41749  sticksstones2  41750  sticksstones3  41751  sticksstones8  41756  sticksstones10  41758  sticksstones11  41759  sticksstones12a  41760  sticksstones15  41764  nnaddcom  41978  nnadddir  41980  nnmulcom  41982  eu6w  42236  ismrc  42263  incssnn0  42273  mzpexpmpt  42307  pell14qrexpclnn0  42428  monotuz  42504  rmxypos  42510  jm2.17a  42523  jm2.17b  42524  rmygeid  42527  jm2.18  42551  jm2.19lem3  42554  jm2.25  42562  jm2.15nn0  42566  jm2.16nn0  42567  wepwsolem  42608  aomclem8  42627  dfac11  42628  pwslnm  42660  lnr2i  42682  hbtlem5  42694  cnsrexpcl  42731  rngunsnply  42739  unielss  42788  onsucf1lem  42840  cantnfresb  42895  onmcl  42902  naddonnn  42967  elmapintrab  43148  elmapintab  43168  cnvcnvintabd  43172  eliunov2  43251  relexpxpnnidm  43275  relexpiidm  43276  relexpss1d  43277  iunrelexpmin1  43280  relexpmulnn  43281  iunrelexpmin2  43284  relexp0a  43288  trclimalb2  43298  clsk3nimkb  43612  ntrclsiso  43639  ntrclskb  43641  ntrneiiso  43663  ntrneix2  43665  ntrneixb  43667  gneispace2  43704  gneispacess2  43718  mnuunid  43856  dvgrat  43891  pm14.122b  44002  fnchoice  44533  fiiuncl  44571  ssinc  44593  ssdec  44594  wessf1ornlem  44697  dmrelrnrel  44738  fperiodmullem  44823  monoordxrv  45002  fmul01  45106  fmuldfeq  45109  climsuselem1  45133  climinff  45137  ellimcabssub0  45143  limcleqr  45170  addlimc  45174  0ellimcdiv  45175  limclner  45177  limsupref  45211  limsupub  45230  limsupmnf  45247  limsupre2lem  45250  limsupre2  45251  limsupre2mpt  45256  limsupre3lem  45258  limsupre3  45259  limsupre3mpt  45260  xlimbr  45353  cnrefiisplem  45355  dvnmptdivc  45464  dvnmptconst  45467  dvnmul  45469  iblspltprt  45499  itgspltprt  45505  stoweidlem2  45528  stoweidlem3  45529  stoweidlem17  45543  stoweidlem19  45545  stoweidlem21  45547  stoweidlem26  45552  fourierdlem42  45675  issal  45840  ismea  45977  isome  46020  carageniuncllem1  46047  caratheodorylem1  46052  2reu8i  46631  2reuimp0  46632  funressndmafv2rn  46741  2ffzoeq  46845  smonoord  46848  fargshiftf1  46918  ichnfimlem  46940  paireqne  46988  reupr  46999  reuopreuprim  47003  perfectALTVlem2  47199  grimcnv  47363  lmodvsmdi  47632  dmatALTval  47654  dmatALTbasel  47656  snlindsntor  47725  ldepsnlinc  47762  elbigo2r  47812  elbigolo1  47816  itcovalt2  47936  mof0  48076  isnrm4  48135  iscnrm3r  48153  iscnrm4  48159  lubsscl  48165  glbsscl  48166  ipolubdm  48184  ipoglbdm  48187  setrecseq  48302  setrec2fun  48309  setrec2lem2  48311