Theorem imbi2d 341

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 273	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  345  imbi2  349  pm5.42  545  orbi2d  915  19.23t  2204  axc14  2463  mojust  2534  mof  2558  eu6lem  2568  nfabdwOLD  2928  2gencl  3517  3gencl  3518  vtocl2gf  3561  vtocl3gf  3562  vtocl2g  3563  vtocl3g  3564  vtocl2ga  3567  vtocl4g  3572  eqeu  3702  mo2icl  3710  euind  3720  reu7  3728  reuind  3749  sbctt  3853  reu8nf  3871  sbcnestgfw  4418  sbcnestgf  4423  r19.36zv  4506  dedth2h  4587  dedth3h  4588  dedth4h  4589  reusngf  4676  reuprg0  4706  preq12bg  4854  elint  4956  elintrabg  4965  intab  4982  axrep1  5286  axreplem  5287  axrep2  5288  axrep6g  5293  bm1.3ii  5302  reusv3  5403  poclOLD  5596  swopolem  5598  solin  5613  freq1  5646  frminex  5656  vtoclr  5738  2optocl  5770  3optocl  5771  raliunxp  5838  resieq  5991  iss  6034  cnveqb  6193  reu3op  6289  reuop  6290  dfpo2  6293  preddowncl  6331  funmoOLD  6562  funimaexgOLD  6633  fnbrfvb  6942  fvelimab  6962  fvmptss  7008  fmptco  7124  fprg  7150  fnressn  7153  fressnfv  7155  isoselem  7335  ovg  7569  caovcan  7608  caovordig  7609  caovord  7615  tfisi  7845  tfindsg  7847  tfinds2  7850  tfinds3  7851  dfom2  7854  elom  7855  findsg  7887  finds2  7888  f1o2ndf1  8105  poxp  8111  fnse  8116  xpord3inddlem  8137  soseq  8142  fpr3g  8267  frrlem12  8279  fpr2a  8284  wfr3g  8304  wfrlem4OLD  8309  smoeq  8347  smores  8349  smogt  8364  tfrlem1  8373  tfr3  8396  oaordi  8543  oeordi  8584  oeoa  8594  oeoe  8596  nnacl  8608  nnmcl  8609  nnecl  8610  nnacom  8614  nnaordi  8615  nnawordi  8618  nnaass  8619  nndi  8620  nnmass  8621  nnmsucr  8622  nnmcom  8623  nnmordi  8628  naddssim  8681  2ecoptocl  8799  3ecoptocl  8800  undifixp  8925  xpdom2g  9065  findcard2  9161  unfi  9169  ssfi  9170  imafi  9172  fnfi  9178  findcard2OLD  9281  xpfiOLD  9315  fodomfi  9322  finsschain  9356  marypha1lem  9425  marypha1  9426  supeq1  9437  ordiso2  9507  ordtypelem7  9516  wemaplem1  9538  inf3lem2  9621  inf3lem5  9624  infdiffi  9650  cantnfval2  9661  cantnfle  9663  cantnfp1lem3  9672  oemapval  9675  cantnflem1  9681  cantnf  9685  wemapwe  9689  cnfcom  9692  cnfcom3clem  9697  ttrclss  9712  ttrclselem2  9718  tz9.1  9721  frr3g  9748  frr2  9752  r1pwALT  9838  cplem2  9882  karden  9887  updjud  9926  infxpenc2lem2  10012  fseqenlem1  10016  dfac8clem  10024  alephinit  10087  dfac4  10114  dfac5lem5  10119  dfac2a  10121  dfac2b  10122  dfacacn  10133  dfac12lem3  10137  kmlem2  10143  kmlem13  10154  nnadju  10189  ackbij1lem16  10227  sornom  10269  infpssrlem4  10298  fin23lem14  10325  fin23lem32  10336  fin23lem34  10338  fin23lem36  10340  isf32lem1  10345  isf32lem2  10346  axcc2lem  10428  axcc3  10430  axcclem  10449  zornn0g  10497  ttukeylem5  10505  ttukeylem6  10506  axrepnd  10586  axpowndlem3  10591  zfcndrep  10606  fpwwe2lem7  10629  pwfseqlem3  10652  wunr1om  10711  wunfi  10713  tskr1om  10759  ingru  10807  grudomon  10809  axgroth3  10823  axgroth4  10824  nqereu  10921  mulcanenq  10952  elnp  10979  elnpi  10980  prlem934  11025  infm3  12170  nnindd  12229  nnaddcl  12232  nnmulcl  12233  nnne0  12243  peano5uzi  12648  uzind2  12652  nn0indd  12656  zindd  12660  fzindd  12661  eluzaddOLD  12854  uzaddcl  12885  uzwo  12892  indstr  12897  zmax  12926  xmulasslem  13261  xrsupsslem  13283  xrinfmsslem  13284  xrsupss  13285  xrinfmss  13286  flval2  13776  om2uzlti  13912  uzrdgfni  13920  rabssnn0fi  13948  mptnn0fsupp  13959  seqcl2  13983  seqfveq2  13987  seqshft2  13991  monoord  13995  seqsplit  13998  seqcaopr3  14000  seqf1olem2a  14003  seqf1o  14006  seqid2  14011  seqhomo  14012  ser1const  14021  expcllem  14035  expeq0  14055  mulexp  14064  expadd  14067  expmul  14070  expmordi  14129  leexp2r  14136  leexp1a  14137  bernneq  14189  modexp  14198  facdiv  14244  faclbnd  14247  faclbnd4lem4  14253  hashgadd  14334  hashxp  14391  hashmap  14392  hashf1lem2  14414  hashf1  14415  seqcoll  14422  wrdind  14669  wrd2ind  14670  pfxccatin12lem3  14679  cshweqrep  14768  2cshwcshw  14773  relexp0g  14966  relexpsucnnr  14969  relexpsucnnl  14974  relexpcnv  14979  relexpnndm  14985  relexpaddnn  14995  rtrclreclem1  15001  dfrtrclrec2  15002  rtrclreclem2  15003  rtrclreclem4  15005  dfrtrcl2  15006  relexpind  15008  reusq0  15406  rlim  15436  rlim2  15437  rlim0  15449  rlim0lt  15450  rlimi  15454  ello12r  15458  ello1mpt  15462  ello1d  15464  elo12r  15469  lo1o1  15473  o1lo1  15478  lo1res  15500  climshft  15517  o1compt  15528  rlimo1  15558  lo1add  15568  lo1mul  15569  rlimdiv  15589  climub  15605  climserle  15606  caucvgrlem  15616  caurcvgr  15617  iseraltlem2  15626  summolem2a  15658  sumss  15667  fsum2d  15714  fsumabs  15744  fsumrlim  15754  fsumo1  15755  fsumiun  15764  binom  15773  climcndslem1  15792  climcndslem2  15793  cvgrat  15826  clim2prod  15831  prodfn0  15837  prodfrec  15838  ntrivcvgfvn0  15842  prodmolem2a  15875  fprodabs  15915  fprodn0  15920  fprod2d  15922  binomfallfac  15982  bpolycl  15993  bpolydif  15996  fprodefsum  16035  demoivreALT  16141  ruclem8  16177  ruclem9  16178  dvdsle  16250  dvdsfac  16266  divalglem7  16339  bitsinv1  16380  sadcadd  16396  sadadd2  16398  saddisjlem  16402  smuval2  16420  smupvallem  16421  smu01lem  16423  smupval  16426  smueqlem  16428  smumullem  16430  bezoutlem4  16481  dfgcd2  16485  rplpwr  16496  nn0seqcvgd  16504  seq1st  16505  alginv  16509  algcvga  16513  algfx  16514  lcmf  16567  prmind2  16619  prmdvdsexp  16649  prmfac1  16655  reumodprminv  16734  pcmpt  16822  pcfac  16829  prmpwdvds  16834  prmreclem4  16849  vdwlem10  16920  ramval  16938  ramcl  16959  cshwrepswhash1  17033  prmlem1a  17037  imasleval  17484  ismre  17531  mreexexd  17589  lubprop  18308  lublecllem  18310  glbprop  18321  joinlem  18333  meetlem  18347  poslubmo  18361  posglbmo  18362  poslubd  18363  isglbd  18459  lubun  18465  mndind  18706  frmdgsum  18740  mulgnnass  18984  mhmmulg  18990  gsumwrev  19228  gsmsymgrfix  19291  gsmsymgreq  19295  psgnunilem3  19359  sylow1lem1  19461  efginvrel2  19590  efgsrel  19597  efgredlemd  19607  efgredlem  19610  efgred  19611  efgrelexlemb  19613  gsum2dlem2  19834  gsumcom2  19838  ablfac1eulem  19937  pgpfac1lem2  19940  pgpfac1lem5  19944  pgpfac1  19945  pgpfac  19949  srgmulgass  20034  srgpcomp  20035  srgbinom  20048  lmodvsmmulgdi  20500  isdomn2  20908  cnfldexp  20971  islindf4  21385  assamulgscm  21447  mplcoe1  21584  mplcoe3  21585  mplcoe5  21587  gsummoncoe1  21820  dmatval  21986  dmatel  21987  dmatmulcl  21994  pmatcoe1fsupp  22195  decpmataa0  22262  decpmatmulsumfsupp  22267  pmatcollpw2lem  22271  pm2mpmhmlem1  22312  fiinopn  22395  mretopd  22588  neiptoptop  22627  cnpfval  22730  iscnp3  22740  tgcn  22748  lmbr  22754  lmbr2  22755  lmbrf  22756  lmss  22794  ishaus  22818  hausnei2  22849  t1sep2  22865  fiuncmp  22900  dfconn2  22915  1stcfb  22941  2ndc1stc  22947  1stcrest  22949  1stcelcls  22957  1stccn  22959  lly1stc  22992  elkgen  23032  kgencn  23052  tx1stc  23146  xkopt  23151  cnmptcom  23174  isr0  23233  r0sep  23244  ptcmpfi  23309  isfildlem  23353  rnelfm  23449  fbflim  23472  flimrest  23479  isflf  23489  flffbas  23491  lmflf  23501  fclsrest  23520  isfcf  23530  cnextfvval  23561  tmdgsum  23591  eltsms  23629  tsmsi  23630  tsmsgsum  23635  tsmssubm  23639  tsmsres  23640  tsmsf1o  23641  isust  23700  isucn  23775  isucn2  23776  ucnima  23778  imasdsf1olem  23871  metss  24009  met1stc  24022  metcnp  24042  metcnpi  24045  metcnpi2  24046  metucn  24072  xrge0tsms  24342  fsumcn  24378  elcncf  24397  cncfi  24402  rescncf  24405  cncfco  24415  caucfil  24792  equivcau  24809  caubl  24817  caublcls  24818  ovolgelb  24989  ovolunlem1a  25005  ovolicc2lem3  25028  voliunlem1  25059  voliunlem3  25061  volsuplem  25064  volsup  25065  dyadmax  25107  vitali  25122  itg2leub  25244  itgfsum  25336  dvnadd  25438  dvnres  25440  cpnord  25444  dvnfre  25461  dvmptfsum  25484  dvferm1  25494  dvferm2  25496  rolle  25499  dvlip  25502  c1lip1  25506  lhop1  25523  deg1leb  25605  ply1divex  25646  fta1g  25677  plyco  25747  dgrcolem1  25779  dgrco  25781  dvnply2  25792  plydivex  25802  aalioulem2  25838  aalioulem3  25839  aalioulem5  25841  aaliou3lem2  25848  dvntaylp  25875  taylthlem1  25877  ulmdvlem3  25906  abelthlem9  25944  cxpmul2  26189  scvxcvx  26480  jensenlem2  26482  jensen  26483  wilthlem3  26564  perfectlem2  26723  bcmono  26770  bposlem5  26781  lgsquad2lem2  26878  addsq2reu  26933  2sqreulem1  26939  2sqreunnlem1  26942  dchrisumlem1  26982  dchrisum0flb  27003  pntpbnd1  27079  pntlemf  27098  qabvle  27118  qabvexp  27119  ostthlem2  27121  ostth2lem2  27127  nosupcbv  27195  nosupno  27196  nosupdm  27197  nosupfv  27199  nosupres  27200  nosupbnd1lem1  27201  nosupbnd1lem3  27203  nosupbnd1lem5  27205  noinfcbv  27210  noinfno  27211  noinfdm  27212  noinffv  27214  noinfres  27215  noinfbnd1lem3  27218  noinfbnd1lem5  27220  eqscut2  27297  addsproplem1  27443  addsprop  27450  negsunif  27519  mulsproplem9  27570  ssltmul2  27593  precsexlem8  27650  precsexlem9  27651  precsexlem11  27653  tgcgr4  27772  usgr2pth  29011  wlkiswwlks2lem4  29116  wlkiswwlks2  29119  rusgrnumwwlk  29219  clwlkclwwlklem2a  29241  clwlkclwwlklem1  29242  clwlkclwwlkfo  29252  eupth2  29482  frgr3vlem1  29516  3vfriswmgrlem  29520  3vfriswmgr  29521  wlkl0  29610  numclwlk2lem2f1o  29622  isplig  29717  isnvlem  29851  nvi  29855  nmoubi  30013  nmounbi  30017  nmblolbi  30041  ipasslem1  30072  ipassi  30082  hlim2  30433  pjhth  30634  spansni  30798  elspansn2  30808  pjige0  30932  pjcjt2  30933  pjopyth  30961  elcnop  31098  elcnfn  31123  nmopub  31149  cnopc  31154  nmfnleub  31166  elnlfn  31169  cnfnc  31171  nmbdoplb  31266  nmcexi  31267  nmcoplb  31271  lnfnmul  31289  nmbdfnlb  31291  nmcfnlb  31295  pjss2coi  31405  pjssmi  31406  isst  31454  ishst  31455  stcltr1i  31515  mdbr  31535  dmdbr  31540  mddmd2  31550  mdslmd1lem3  31568  mdslmd1lem4  31569  elat2  31581  atcvat2  31630  cdj1i  31674  iuninc  31780  fmptcof2  31870  nn0min  32014  wrdt2ind  32105  ismnt  32141  xrge0tsmsd  32197  isomnd  32207  omndadd  32212  cyc3genpm  32299  isarchi2  32319  archirng  32322  archiexdiv  32324  archiabl  32332  isorng  32406  ofldchr  32421  islbs5  32485  mxidlval  32566  crefeq  32814  nexple  32996  esumfzf  33056  issiga  33099  isrnsiga  33100  isldsys  33143  ismeas  33186  isrnmeas  33187  measiun  33205  eulerpartlemn  33369  sseqp1  33383  rrvsum  33442  signsply0  33551  signstfvc  33574  bnj941  33772  bnj106  33868  bnj155  33879  bnj590  33910  bnj591  33911  bnj849  33925  bnj893  33928  bnj944  33938  bnj1128  33990  subfacp1lem6  34165  erdszelem8  34178  issconn  34206  cvmliftlem7  34271  cvmliftlem10  34274  cvmlift3lem2  34300  satfsschain  34344  satfrel  34347  satfdm  34349  satfrnmapom  34350  fmlafvel  34365  satffun  34389  mrsubvrs  34502  mclsssvlem  34542  mclsval  34543  mclsax  34549  mclsind  34550  shftvalg  34690  bccolsum  34698  iprodefisumlem  34699  faclimlem1  34702  rdgprc  34755  fveleq  35325  unblimceq0  35372  bj-ax12  35523  bj-bm1.3ii  35934  rdgeqoa  36240  finxpreclem6  36266  domalom  36274  ralssiun  36277  wl-sblimt  36405  wl-sbhbt  36408  wl-2sb6d  36412  wl-mo2df  36424  wl-mo2t  36429  poimirlem2  36479  poimirlem25  36502  poimirlem28  36505  poimirlem31  36508  heicant  36512  mbfresfi  36523  itg2gt0cn  36532  sdclem2  36599  fdc  36602  seqpo  36604  incsequz  36605  mettrifi  36614  prdsbnd2  36652  heiborlem4  36671  bfplem1  36679  iscringd  36855  maxidlval  36896  igenval2  36923  iss2  37202  elrefrels3  37378  ax12eq  37800  ax12el  37801  ax12indalem  37804  ax12inda2ALT  37805  ax12inda  37807  ax12v2-o  37808  riotasvd  37815  isopos  38039  isat3  38166  ishlat1  38211  glbconN  38236  glbconNOLD  38237  ispsubsp  38605  isldil  38970  isltrn  38979  isdilN  39014  trlval  39022  cdleme27b  39228  cdleme29b  39235  cdleme31sn1  39241  cdleme31sn1c  39248  cdleme40v  39329  cdlemk36  39773  cdlemkid5  39795  cdlemn11pre  40070  dihord2pre  40085  islpolN  40343  hdmapffval  40686  hdmapfval  40687  hdmapval2lem  40691  uzindd  40831  sticksstones1  40951  sticksstones2  40952  sticksstones3  40953  sticksstones8  40958  sticksstones10  40960  sticksstones11  40961  sticksstones12a  40962  sticksstones15  40966  nnaddcom  41180  nnadddir  41182  nnmulcom  41184  ismrc  41425  incssnn0  41435  mzpexpmpt  41469  pell14qrexpclnn0  41590  monotuz  41666  rmxypos  41672  jm2.17a  41685  jm2.17b  41686  rmygeid  41689  jm2.18  41713  jm2.19lem3  41716  jm2.25  41724  jm2.15nn0  41728  jm2.16nn0  41729  wepwsolem  41770  aomclem8  41789  dfac11  41790  pwslnm  41822  lnr2i  41844  hbtlem5  41856  cnsrexpcl  41893  rngunsnply  41901  isdomn3  41932  unielss  41953  onsucf1lem  42005  cantnfresb  42060  onmcl  42067  naddonnn  42132  elmapintrab  42313  elmapintab  42333  cnvcnvintabd  42337  eliunov2  42416  relexpxpnnidm  42440  relexpiidm  42441  relexpss1d  42442  iunrelexpmin1  42445  relexpmulnn  42446  iunrelexpmin2  42449  relexp0a  42453  trclimalb2  42463  clsk3nimkb  42777  ntrclsiso  42804  ntrclskb  42806  ntrneiiso  42828  ntrneix2  42830  ntrneixb  42832  gneispace2  42869  gneispacess2  42883  mnuunid  43022  dvgrat  43057  pm14.122b  43168  fnchoice  43699  fiiuncl  43738  ssinc  43762  ssdec  43763  wessf1ornlem  43868  dmrelrnrel  43911  fperiodmullem  44000  monoordxrv  44179  fmul01  44283  fmuldfeq  44286  climsuselem1  44310  climinff  44314  ellimcabssub0  44320  limcleqr  44347  addlimc  44351  0ellimcdiv  44352  limclner  44354  limsupref  44388  limsupub  44407  limsupmnf  44424  limsupre2lem  44427  limsupre2  44428  limsupre2mpt  44433  limsupre3lem  44435  limsupre3  44436  limsupre3mpt  44437  xlimbr  44530  cnrefiisplem  44532  dvnmptdivc  44641  dvnmptconst  44644  dvnmul  44646  iblspltprt  44676  itgspltprt  44682  stoweidlem2  44705  stoweidlem3  44706  stoweidlem17  44720  stoweidlem19  44722  stoweidlem21  44724  stoweidlem26  44729  fourierdlem42  44852  issal  45017  ismea  45154  isome  45197  carageniuncllem1  45224  caratheodorylem1  45229  2reu8i  45808  2reuimp0  45809  funressndmafv2rn  45918  2ffzoeq  46023  smonoord  46026  fargshiftf1  46096  ichnfimlem  46118  paireqne  46166  reupr  46177  reuopreuprim  46181  perfectALTVlem2  46377  lmodvsmdi  47012  dmatALTval  47035  dmatALTbasel  47037  snlindsntor  47106  ldepsnlinc  47143  elbigo2r  47193  elbigolo1  47197  itcovalt2  47317  mof0  47458  isnrm4  47517  iscnrm3r  47535  iscnrm4  47541  lubsscl  47547  glbsscl  47548  ipolubdm  47566  ipoglbdm  47569  setrecseq  47684  setrec2fun  47691  setrec2lem2  47693