Theorem imbi2d 333

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  imbi12d  337  imbi2  341  pm5.42  536  orbi2d  899  con3ALTOLD  1066  19.23t  2137  axc15OLD  2356  axc14  2398  mojust  2543  mof  2571  mofOLD  2572  eu6lem  2584  eu6OLD  2587  2gencl  3450  3gencl  3451  vtocl2gf  3482  vtocl3gf  3483  vtocl2g  3484  vtocl2ga  3488  vtocl4g  3492  eqeu  3605  mo2icl  3615  euind  3623  reu7  3631  reuind  3649  sbctt  3743  reu8nf  3759  sbcnestgf  4253  r19.36zv  4329  dedth2h  4401  dedth3h  4402  dedth4h  4403  reusngf  4480  reuprg0  4506  preq12bg  4652  elint  4749  elintrabg  4756  intab  4773  axrep1  5044  axreplem  5045  axrep2  5046  bm1.3ii  5057  reusv3  5153  pocl  5326  swopolem  5328  solin  5343  freq1  5370  frminex  5380  vtoclr  5458  2optocl  5489  3optocl  5490  raliunxp  5553  resieq  5703  iss  5742  cnveqb  5886  reu3op  5975  reuop  5976  preddowncl  6007  funmo  6198  funimaexg  6267  fnbrfvb  6542  fvelimab  6560  fvmptss  6600  fmptco  6708  fprg  6734  fnressn  6737  fressnfv  6739  isoselem  6911  ovg  7123  caovcan  7162  caovordig  7163  caovord  7169  tfisi  7383  tfindsg  7385  tfinds2  7388  tfinds3  7389  dfom2  7392  elom  7393  findsg  7418  finds2  7419  f1o2ndf1  7616  poxp  7620  fnse  7625  wfr3g  7749  wfrlem4  7754  wfrlem4OLD  7755  smoeq  7784  smores  7786  smogt  7801  tfrlem1  7809  tfr3  7832  oaordi  7965  oeordi  8006  oeoa  8016  oeoe  8018  nnacl  8030  nnmcl  8031  nnecl  8032  nnacom  8036  nnaordi  8037  nnawordi  8040  nnaass  8041  nndi  8042  nnmass  8043  nnmsucr  8044  nnmcom  8045  nnmordi  8050  2ecoptocl  8180  3ecoptocl  8181  undifixp  8287  xpdom2g  8401  findcard2  8545  xpfi  8576  fnfi  8583  fodomfi  8584  finsschain  8618  marypha1lem  8684  marypha1  8685  supeq1  8696  ordiso2  8766  ordtypelem7  8775  wemaplem1  8797  inf3lem2  8878  inf3lem5  8881  infdiffi  8907  cantnfval2  8918  cantnfle  8920  cantnfp1lem3  8929  oemapval  8932  cantnflem1  8938  cantnf  8942  wemapwe  8946  cnfcom  8949  cnfcom3clem  8954  tz9.1  8957  r1pwALT  9061  cplem2  9105  karden  9110  updjud  9149  infxpenc2lem2  9232  fseqenlem1  9236  dfac8clem  9244  alephinit  9307  dfac4  9334  dfac5lem5  9339  dfac2a  9341  dfac2b  9342  dfacacn  9353  dfac12lem3  9357  kmlem2  9363  kmlem13  9374  ackbij1lem16  9447  sornom  9489  infpssrlem4  9518  fin23lem14  9545  fin23lem32  9556  fin23lem34  9558  fin23lem36  9560  isf32lem1  9565  isf32lem2  9566  axcc2lem  9648  axcc3  9650  axcclem  9669  zornn0g  9717  ttukeylem5  9725  ttukeylem6  9726  axrepnd  9806  axpowndlem3  9811  zfcndrep  9826  fpwwe2lem8  9849  pwfseqlem3  9872  wunr1om  9931  wunfi  9933  tskr1om  9979  ingru  10027  grudomon  10029  axgroth3  10043  axgroth4  10044  nqereu  10141  mulcanenq  10172  elnp  10199  elnpi  10200  prlem934  10245  infm3  11393  nnaddcl  11455  nnmulcl  11456  nnmulclOLD  11457  nnne0  11467  peano5uzi  11877  uzind2  11881  nn0indd  11885  zindd  11889  eluzadd  12080  uzaddcl  12111  uzwo  12118  indstr  12123  zmax  12152  xmulasslem  12487  xrsupsslem  12509  xrinfmsslem  12510  xrsupss  12511  xrinfmss  12512  flval2  12992  om2uzlti  13126  uzrdgfni  13134  rabssnn0fi  13162  mptnn0fsupp  13173  seqcl2  13196  seqfveq2  13200  seqshft2  13204  monoord  13208  seqsplit  13211  seqcaopr3  13213  seqf1olem2a  13216  seqf1o  13219  seqid2  13224  seqhomo  13225  ser1const  13234  expcllem  13248  expeq0  13267  mulexp  13276  expadd  13279  expmul  13282  expmordi  13339  leexp2r  13346  leexp1a  13347  bernneq  13398  modexp  13407  facdiv  13455  faclbnd  13458  faclbnd4lem4  13464  hashgadd  13544  hashxp  13598  hashmap  13599  hashf1lem2  13617  hashf1  13618  seqcoll  13625  wrdind  13905  wrdindOLD  13906  wrd2ind  13907  wrd2indOLD  13908  swrdccatin12lem3  13923  cshweqrep  14035  2cshwcshw  14039  relexp0g  14232  relexpsucnnr  14235  relexpsucnnl  14242  relexpcnv  14245  relexpnndm  14251  relexpaddnn  14261  dfrtrclrec2  14267  rtrclreclem1  14268  rtrclreclem2  14269  rtrclreclem4  14271  dfrtrcl2  14272  relexpind  14274  reusq0  14673  rlim  14703  rlim2  14704  rlim0  14716  rlim0lt  14717  rlimi  14721  ello12r  14725  ello1mpt  14729  ello1d  14731  elo12r  14736  lo1o1  14740  o1lo1  14745  lo1res  14767  climshft  14784  o1compt  14795  rlimo1  14824  lo1add  14834  lo1mul  14835  rlimdiv  14853  climub  14869  climserle  14870  caucvgrlem  14880  caurcvgr  14881  iseraltlem2  14890  summolem2a  14922  sumss  14931  fsum2d  14976  fsumabs  15006  fsumrlim  15016  fsumo1  15017  fsumiun  15026  binom  15035  climcndslem1  15054  climcndslem2  15055  cvgrat  15089  clim2prod  15094  prodfn0  15100  prodfrec  15101  ntrivcvgfvn0  15105  prodmolem2a  15138  fprodabs  15178  fprodn0  15183  fprod2d  15185  binomfallfac  15245  bpolycl  15256  bpolydif  15259  fprodefsum  15298  demoivreALT  15404  ruclem8  15440  ruclem9  15441  dvdsle  15510  dvdsfac  15526  divalglem7  15600  bitsinv1  15641  sadcadd  15657  sadadd2  15659  saddisjlem  15663  smuval2  15681  smupvallem  15682  smu01lem  15684  smupval  15687  smueqlem  15689  smumullem  15691  bezoutlem4  15736  dfgcd2  15740  gcdmultiple  15746  rplpwr  15753  nn0seqcvgd  15760  seq1st  15761  alginv  15765  algcvga  15769  algfx  15770  lcmf  15823  prmind2  15875  prmdvdsexp  15905  prmfac1  15909  reumodprminv  15987  pcmpt  16074  pcfac  16081  prmpwdvds  16086  prmreclem4  16101  vdwlem10  16172  ramval  16190  ramcl  16211  cshwrepswhash1  16282  prmlem1a  16286  imasleval  16660  ismre  16709  mreexexd  16767  lubprop  17444  lublecllem  17446  glbprop  17457  joinlem  17469  meetlem  17483  isglbd  17575  lubun  17581  poslubmo  17604  posglbmo  17605  poslubd  17606  mndind  17824  frmdgsum  17858  mulgnnass  18036  mhmmulg  18042  gsumwrev  18255  gsmsymgrfix  18307  gsmsymgreq  18311  psgnunilem3  18376  sylow1lem1  18474  efginvrel2  18601  efgsrel  18608  efgredlemd  18619  efgredlem  18622  efgredlemOLD  18623  efgred  18624  efgrelexlemb  18626  gsum2dlem2  18834  gsumcom2  18838  ablfac1eulem  18934  pgpfac1lem2  18937  pgpfac1lem5  18941  pgpfac1  18942  pgpfac  18946  srgmulgass  18994  srgpcomp  18995  srgbinom  19008  lmodvsmmulgdi  19381  isdomn2  19783  assamulgscm  19834  mplcoe1  19949  mplcoe3  19950  mplcoe5  19952  gsummoncoe1  20165  cnfldexp  20270  islindf4  20674  dmatval  20795  dmatel  20796  dmatmulcl  20803  pmatcoe1fsupp  21003  decpmataa0  21070  decpmatmulsumfsupp  21075  pmatcollpw2lem  21079  pm2mpmhmlem1  21120  fiinopn  21203  mretopd  21394  neiptoptop  21433  cnpfval  21536  iscnp3  21546  tgcn  21554  lmbr  21560  lmbr2  21561  lmbrf  21562  lmss  21600  ishaus  21624  hausnei2  21655  t1sep2  21671  fiuncmp  21706  dfconn2  21721  1stcfb  21747  2ndc1stc  21753  1stcrest  21755  1stcelcls  21763  1stccn  21765  lly1stc  21798  elkgen  21838  kgencn  21858  tx1stc  21952  xkopt  21957  cnmptcom  21980  isr0  22039  r0sep  22050  ptcmpfi  22115  isfildlem  22159  rnelfm  22255  fbflim  22278  flimrest  22285  isflf  22295  flffbas  22297  lmflf  22307  fclsrest  22326  isfcf  22336  cnextfvval  22367  tmdgsum  22397  eltsms  22434  tsmsi  22435  tsmsgsum  22440  tsmssubm  22444  tsmsres  22445  tsmsf1o  22446  isust  22505  isucn  22580  isucn2  22581  ucnima  22583  imasdsf1olem  22676  metss  22811  met1stc  22824  metcnp  22844  metcnpi  22847  metcnpi2  22848  metucn  22874  xrge0tsms  23135  fsumcn  23171  elcncf  23190  cncfi  23195  rescncf  23198  cncfco  23208  caucfil  23579  equivcau  23596  caubl  23604  caublcls  23605  ovolgelb  23774  ovolunlem1a  23790  ovolicc2lem3  23813  voliunlem1  23844  voliunlem3  23846  volsuplem  23849  volsup  23850  dyadmax  23892  vitali  23907  itg2leub  24028  itgfsum  24120  dvnadd  24219  dvnres  24221  cpnord  24225  dvnfre  24242  dvmptfsum  24265  dvferm1  24275  dvferm2  24277  rolle  24280  dvlip  24283  c1lip1  24287  lhop1  24304  deg1leb  24382  ply1divex  24423  fta1g  24454  plyco  24524  dgrcolem1  24556  dgrco  24558  dvnply2  24569  plydivex  24579  aalioulem2  24615  aalioulem3  24616  aalioulem5  24618  aaliou3lem2  24625  dvntaylp  24652  taylthlem1  24654  ulmdvlem3  24683  abelthlem9  24721  cxpmul2  24963  scvxcvx  25255  jensenlem2  25257  jensen  25258  wilthlem3  25339  perfectlem2  25498  bcmono  25545  bposlem5  25556  lgsquad2lem2  25653  addsq2reu  25708  2sqreulem1  25714  2sqreunnlem1  25717  dchrisumlem1  25757  dchrisum0flb  25778  pntpbnd1  25854  pntlemf  25873  qabvle  25893  qabvexp  25894  ostthlem2  25896  ostth2lem2  25902  tgcgr4  26009  usgr2pth  27243  wlkiswwlks2lem4  27348  wlkiswwlks2  27351  rusgrnumwwlk  27472  clwlkclwwlklem2a  27494  clwlkclwwlklem1  27495  clwlkclwwlkfoOLD  27509  clwlkclwwlkfo  27513  eupth2  27759  frgr3vlem1  27797  3vfriswmgrlem  27801  3vfriswmgr  27802  wlkl0  27910  numclwlk2lem2f1o  27922  numclwlk2lem2f1oOLD  27925  isplig  28020  isnvlem  28154  nvi  28158  nmoubi  28316  nmounbi  28320  nmblolbi  28344  ipasslem1  28375  ipassi  28385  hlim2  28738  pjhth  28941  spansni  29105  elspansn2  29115  pjige0  29239  pjcjt2  29240  pjopyth  29268  elcnop  29405  elcnfn  29430  nmopub  29456  cnopc  29461  nmfnleub  29473  elnlfn  29476  cnfnc  29478  nmbdoplb  29573  nmcexi  29574  nmcoplb  29578  lnfnmul  29596  nmbdfnlb  29598  nmcfnlb  29602  pjss2coi  29712  pjssmi  29713  isst  29761  ishst  29762  stcltr1i  29822  mdbr  29842  dmdbr  29847  mddmd2  29857  mdslmd1lem3  29875  mdslmd1lem4  29876  elat2  29888  atcvat2  29937  cdj1i  29981  vtocl2d  30003  iuninc  30071  fmptcof2  30154  nnindd  30271  nn0min  30272  isomnd  30398  omndadd  30403  isarchi2  30436  archirng  30439  archiexdiv  30441  archiabl  30449  xrge0tsmsd  30486  isorng  30507  ofldchr  30522  crefeq  30710  nexple  30869  esumfzf  30929  issiga  30972  isrnsiga  30974  isldsys  31017  ismeas  31060  isrnmeas  31061  measiun  31079  eulerpartlemn  31241  sseqp1  31256  rrvsum  31315  signsply0  31428  signstfvc  31452  bnj941  31653  bnj106  31748  bnj155  31759  bnj590  31790  bnj591  31791  bnj849  31805  bnj893  31808  bnj944  31818  bnj1128  31868  subfacp1lem6  31977  erdszelem8  31990  issconn  32018  cvmliftlem7  32083  cvmliftlem10  32086  cvmlift3lem2  32112  mrsubvrs  32229  mclsssvlem  32269  mclsval  32270  mclsax  32276  mclsind  32277  shftvalg  32423  bccolsum  32431  iprodefisumlem  32432  faclimlem1  32435  dfpo2  32451  rdgprc  32500  trpredmintr  32531  frmin  32545  soseq  32557  frr3g  32582  fpr3g  32583  frrlem12  32595  fpr2  32601  frr2  32606  nosupno  32664  nosupdm  32665  nosupfv  32667  nosupres  32668  nosupbnd1lem1  32669  nosupbnd1lem3  32671  nosupbnd1lem5  32673  noeta  32683  fveleq  33259  unblimceq0  33306  bj-ax12  33436  bj-axrep1  33558  bj-axrep2  33559  bj-axrep3  33560  bj-bm1.3ii  33801  rdgeqoa  34028  finxpreclem6  34053  domalom  34061  ralssiun  34064  wl-sblimt  34164  wl-sbhbt  34167  wl-2sb6d  34171  wl-mo2df  34195  wl-mo2t  34200  poimirlem2  34283  poimirlem25  34306  poimirlem28  34309  poimirlem31  34312  heicant  34316  mbfresfi  34327  itg2gt0cn  34336  sdclem2  34407  fdc  34410  seqpo  34412  incsequz  34413  mettrifi  34422  prdsbnd2  34463  heiborlem4  34482  bfplem1  34490  iscringd  34666  maxidlval  34707  igenval2  34734  iss2  34995  elrefrels3  35151  ax12eq  35470  ax12el  35471  ax12indalem  35474  ax12inda2ALT  35475  ax12inda  35477  ax12v2-o  35478  riotasvd  35485  isopos  35709  isat3  35836  ishlat1  35881  glbconN  35906  ispsubsp  36274  isldil  36639  isltrn  36648  isdilN  36683  trlval  36691  cdleme27b  36897  cdleme29b  36904  cdleme31sn1  36910  cdleme31sn1c  36917  cdleme40v  36998  cdlemk36  37442  cdlemkid5  37464  cdlemn11pre  37739  dihord2pre  37754  islpolN  38012  hdmapffval  38355  hdmapfval  38356  hdmapval2lem  38360  nnaddcom  38541  ismrc  38638  incssnn0  38648  mzpexpmpt  38682  pell14qrexpclnn0  38804  monotuz  38879  rmxypos  38885  jm2.17a  38898  jm2.17b  38899  rmygeid  38902  jm2.18  38926  jm2.19lem3  38929  jm2.25  38937  jm2.15nn0  38941  jm2.16nn0  38942  wepwsolem  38983  aomclem8  39002  dfac11  39003  pwslnm  39035  lnr2i  39057  hbtlem5  39069  cnsrexpcl  39106  rngunsnply  39114  isdomn3  39145  ifpbi23  39179  elmapintrab  39243  elmapintab  39263  cnvcnvintabd  39267  eliunov2  39332  relexpxpnnidm  39356  relexpiidm  39357  relexpss1d  39358  iunrelexpmin1  39361  relexpmulnn  39362  iunrelexpmin2  39365  relexp0a  39369  trclimalb2  39379  clsk3nimkb  39698  ntrclsiso  39725  ntrclskb  39727  ntrneiiso  39749  ntrneix2  39751  ntrneixb  39753  gneispace2  39790  gneispacess2  39804  mnuunid  39933  dvgrat  40004  pm14.122b  40116  fnchoice  40649  fiiuncl  40691  ssinc  40720  ssdec  40721  wessf1ornlem  40815  dmrelrnrel  40861  fperiodmullem  40945  monoordxrv  41135  fmul01  41238  fmuldfeq  41241  climsuselem1  41265  climinff  41269  ellimcabssub0  41275  limcleqr  41302  addlimc  41306  0ellimcdiv  41307  limclner  41309  limsupref  41343  limsupub  41362  limsupmnf  41379  limsupre2lem  41382  limsupre2  41383  limsupre2mpt  41388  limsupre3lem  41390  limsupre3  41391  limsupre3mpt  41392  xlimbr  41485  cnrefiisplem  41487  dvnmptdivc  41599  dvnmptconst  41602  dvnmul  41604  iblspltprt  41634  itgspltprt  41640  stoweidlem2  41664  stoweidlem3  41665  stoweidlem17  41679  stoweidlem19  41681  stoweidlem21  41683  stoweidlem26  41688  fourierdlem42  41811  issal  41976  ismea  42110  isome  42153  carageniuncllem1  42180  caratheodorylem1  42185  2reu8i  42664  2reuimp0  42665  funressndmafv2rn  42774  2ffzoeq  42880  smonoord  42883  fargshiftf1  42919  paireqne  42981  reupr  42992  reuopreuprim  42996  perfectALTVlem2  43195  lmodvsmdi  43736  dmatALTval  43762  dmatALTbasel  43764  snlindsntor  43833  ldepsnlinc  43870  elbigo2r  43921  elbigolo1  43925  setrecseq  44095  setrec2fun  44102  setrec2lem2  44104