Theorem imbi2d 344

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 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  348  imbi2  352  pm5.42  547  orbi2d  913  19.23t  2208  axc14  2475  mojust  2597  mof  2622  eu6lem  2633  nfabdw  2976  2gencl  3482  3gencl  3483  vtocl2gf  3518  vtocl3gf  3519  vtocl2g  3520  vtocl2ga  3523  vtocl4g  3527  eqeu  3645  mo2icl  3653  euind  3663  reu7  3671  reuind  3692  sbctt  3790  reu8nf  3806  vtocl2dOLD  3876  csb0  4314  sbcnestgfw  4326  sbcnestgf  4331  r19.36zv  4410  dedth2h  4482  dedth3h  4483  dedth4h  4484  reusngf  4572  reuprg0  4598  preq12bg  4744  elint  4844  elintrabg  4851  intab  4868  axrep1  5155  axreplem  5156  axrep2  5157  bm1.3ii  5170  reusv3  5271  pocl  5445  swopolem  5447  solin  5462  freq1  5489  frminex  5499  vtoclr  5579  2optocl  5610  3optocl  5611  raliunxp  5674  resieq  5829  iss  5870  cnveqb  6020  reu3op  6111  reuop  6112  preddowncl  6143  funmo  6340  funimaexg  6410  fnbrfvb  6693  fvelimab  6712  fvmptss  6757  fmptco  6868  fprg  6894  fnressn  6897  fressnfv  6899  isoselem  7073  ovg  7293  caovcan  7332  caovordig  7333  caovord  7339  tfisi  7553  tfindsg  7555  tfinds2  7558  tfinds3  7559  dfom2  7562  elom  7563  findsg  7590  finds2  7591  f1o2ndf1  7801  poxp  7805  fnse  7810  wfr3g  7936  wfrlem4  7941  smoeq  7970  smores  7972  smogt  7987  tfrlem1  7995  tfr3  8018  oaordi  8155  oeordi  8196  oeoa  8206  oeoe  8208  nnacl  8220  nnmcl  8221  nnecl  8222  nnacom  8226  nnaordi  8227  nnawordi  8230  nnaass  8231  nndi  8232  nnmass  8233  nnmsucr  8234  nnmcom  8235  nnmordi  8240  2ecoptocl  8371  3ecoptocl  8372  undifixp  8481  xpdom2g  8596  findcard2  8742  xpfi  8773  fnfi  8780  fodomfi  8781  finsschain  8815  marypha1lem  8881  marypha1  8882  supeq1  8893  ordiso2  8963  ordtypelem7  8972  wemaplem1  8994  inf3lem2  9076  inf3lem5  9079  infdiffi  9105  cantnfval2  9116  cantnfle  9118  cantnfp1lem3  9127  oemapval  9130  cantnflem1  9136  cantnf  9140  wemapwe  9144  cnfcom  9147  cnfcom3clem  9152  tz9.1  9155  r1pwALT  9259  cplem2  9303  karden  9308  updjud  9347  infxpenc2lem2  9431  fseqenlem1  9435  dfac8clem  9443  alephinit  9506  dfac4  9533  dfac5lem5  9538  dfac2a  9540  dfac2b  9541  dfacacn  9552  dfac12lem3  9556  kmlem2  9562  kmlem13  9573  nnadju  9608  ackbij1lem16  9646  sornom  9688  infpssrlem4  9717  fin23lem14  9744  fin23lem32  9755  fin23lem34  9757  fin23lem36  9759  isf32lem1  9764  isf32lem2  9765  axcc2lem  9847  axcc3  9849  axcclem  9868  zornn0g  9916  ttukeylem5  9924  ttukeylem6  9925  axrepnd  10005  axpowndlem3  10010  zfcndrep  10025  fpwwe2lem8  10048  pwfseqlem3  10071  wunr1om  10130  wunfi  10132  tskr1om  10178  ingru  10226  grudomon  10228  axgroth3  10242  axgroth4  10243  nqereu  10340  mulcanenq  10371  elnp  10398  elnpi  10399  prlem934  10444  infm3  11587  nnindd  11645  nnaddcl  11648  nnmulcl  11649  nnne0  11659  peano5uzi  12059  uzind2  12063  nn0indd  12067  zindd  12071  eluzadd  12261  uzaddcl  12292  uzwo  12299  indstr  12304  zmax  12333  xmulasslem  12666  xrsupsslem  12688  xrinfmsslem  12689  xrsupss  12690  xrinfmss  12691  flval2  13179  om2uzlti  13313  uzrdgfni  13321  rabssnn0fi  13349  mptnn0fsupp  13360  seqcl2  13384  seqfveq2  13388  seqshft2  13392  monoord  13396  seqsplit  13399  seqcaopr3  13401  seqf1olem2a  13404  seqf1o  13407  seqid2  13412  seqhomo  13413  ser1const  13422  expcllem  13436  expeq0  13455  mulexp  13464  expadd  13467  expmul  13470  expmordi  13527  leexp2r  13534  leexp1a  13535  bernneq  13586  modexp  13595  facdiv  13643  faclbnd  13646  faclbnd4lem4  13652  hashgadd  13734  hashxp  13791  hashmap  13792  hashf1lem2  13810  hashf1  13811  seqcoll  13818  wrdind  14075  wrd2ind  14076  pfxccatin12lem3  14085  cshweqrep  14174  2cshwcshw  14178  relexp0g  14373  relexpsucnnr  14376  relexpsucnnl  14381  relexpcnv  14386  relexpnndm  14392  relexpaddnn  14402  rtrclreclem1  14408  dfrtrclrec2  14409  rtrclreclem2  14410  rtrclreclem4  14412  dfrtrcl2  14413  relexpind  14415  reusq0  14814  rlim  14844  rlim2  14845  rlim0  14857  rlim0lt  14858  rlimi  14862  ello12r  14866  ello1mpt  14870  ello1d  14872  elo12r  14877  lo1o1  14881  o1lo1  14886  lo1res  14908  climshft  14925  o1compt  14936  rlimo1  14965  lo1add  14975  lo1mul  14976  rlimdiv  14994  climub  15010  climserle  15011  caucvgrlem  15021  caurcvgr  15022  iseraltlem2  15031  summolem2a  15064  sumss  15073  fsum2d  15118  fsumabs  15148  fsumrlim  15158  fsumo1  15159  fsumiun  15168  binom  15177  climcndslem1  15196  climcndslem2  15197  cvgrat  15231  clim2prod  15236  prodfn0  15242  prodfrec  15243  ntrivcvgfvn0  15247  prodmolem2a  15280  fprodabs  15320  fprodn0  15325  fprod2d  15327  binomfallfac  15387  bpolycl  15398  bpolydif  15401  fprodefsum  15440  demoivreALT  15546  ruclem8  15582  ruclem9  15583  dvdsle  15652  dvdsfac  15668  divalglem7  15740  bitsinv1  15781  sadcadd  15797  sadadd2  15799  saddisjlem  15803  smuval2  15821  smupvallem  15822  smu01lem  15824  smupval  15827  smueqlem  15829  smumullem  15831  bezoutlem4  15880  dfgcd2  15884  gcdmultipleOLD  15890  rplpwr  15897  nn0seqcvgd  15904  seq1st  15905  alginv  15909  algcvga  15913  algfx  15914  lcmf  15967  prmind2  16019  prmdvdsexp  16049  prmfac1  16053  reumodprminv  16131  pcmpt  16218  pcfac  16225  prmpwdvds  16230  prmreclem4  16245  vdwlem10  16316  ramval  16334  ramcl  16355  cshwrepswhash1  16428  prmlem1a  16432  imasleval  16806  ismre  16853  mreexexd  16911  lubprop  17588  lublecllem  17590  glbprop  17601  joinlem  17613  meetlem  17627  isglbd  17719  lubun  17725  poslubmo  17748  posglbmo  17749  poslubd  17750  mndind  17984  frmdgsum  18019  mulgnnass  18254  mhmmulg  18260  gsumwrev  18486  gsmsymgrfix  18548  gsmsymgreq  18552  psgnunilem3  18616  sylow1lem1  18715  efginvrel2  18845  efgsrel  18852  efgredlemd  18862  efgredlem  18865  efgred  18866  efgrelexlemb  18868  gsum2dlem2  19084  gsumcom2  19088  ablfac1eulem  19187  pgpfac1lem2  19190  pgpfac1lem5  19194  pgpfac1  19195  pgpfac  19199  srgmulgass  19274  srgpcomp  19275  srgbinom  19288  lmodvsmmulgdi  19662  isdomn2  20065  cnfldexp  20124  islindf4  20527  assamulgscm  20587  mplcoe1  20705  mplcoe3  20706  mplcoe5  20708  gsummoncoe1  20933  dmatval  21097  dmatel  21098  dmatmulcl  21105  pmatcoe1fsupp  21306  decpmataa0  21373  decpmatmulsumfsupp  21378  pmatcollpw2lem  21382  pm2mpmhmlem1  21423  fiinopn  21506  mretopd  21697  neiptoptop  21736  cnpfval  21839  iscnp3  21849  tgcn  21857  lmbr  21863  lmbr2  21864  lmbrf  21865  lmss  21903  ishaus  21927  hausnei2  21958  t1sep2  21974  fiuncmp  22009  dfconn2  22024  1stcfb  22050  2ndc1stc  22056  1stcrest  22058  1stcelcls  22066  1stccn  22068  lly1stc  22101  elkgen  22141  kgencn  22161  tx1stc  22255  xkopt  22260  cnmptcom  22283  isr0  22342  r0sep  22353  ptcmpfi  22418  isfildlem  22462  rnelfm  22558  fbflim  22581  flimrest  22588  isflf  22598  flffbas  22600  lmflf  22610  fclsrest  22629  isfcf  22639  cnextfvval  22670  tmdgsum  22700  eltsms  22738  tsmsi  22739  tsmsgsum  22744  tsmssubm  22748  tsmsres  22749  tsmsf1o  22750  isust  22809  isucn  22884  isucn2  22885  ucnima  22887  imasdsf1olem  22980  metss  23115  met1stc  23128  metcnp  23148  metcnpi  23151  metcnpi2  23152  metucn  23178  xrge0tsms  23439  fsumcn  23475  elcncf  23494  cncfi  23499  rescncf  23502  cncfco  23512  caucfil  23887  equivcau  23904  caubl  23912  caublcls  23913  ovolgelb  24084  ovolunlem1a  24100  ovolicc2lem3  24123  voliunlem1  24154  voliunlem3  24156  volsuplem  24159  volsup  24160  dyadmax  24202  vitali  24217  itg2leub  24338  itgfsum  24430  dvnadd  24532  dvnres  24534  cpnord  24538  dvnfre  24555  dvmptfsum  24578  dvferm1  24588  dvferm2  24590  rolle  24593  dvlip  24596  c1lip1  24600  lhop1  24617  deg1leb  24696  ply1divex  24737  fta1g  24768  plyco  24838  dgrcolem1  24870  dgrco  24872  dvnply2  24883  plydivex  24893  aalioulem2  24929  aalioulem3  24930  aalioulem5  24932  aaliou3lem2  24939  dvntaylp  24966  taylthlem1  24968  ulmdvlem3  24997  abelthlem9  25035  cxpmul2  25280  scvxcvx  25571  jensenlem2  25573  jensen  25574  wilthlem3  25655  perfectlem2  25814  bcmono  25861  bposlem5  25872  lgsquad2lem2  25969  addsq2reu  26024  2sqreulem1  26030  2sqreunnlem1  26033  dchrisumlem1  26073  dchrisum0flb  26094  pntpbnd1  26170  pntlemf  26189  qabvle  26209  qabvexp  26210  ostthlem2  26212  ostth2lem2  26218  tgcgr4  26325  usgr2pth  27553  wlkiswwlks2lem4  27658  wlkiswwlks2  27661  rusgrnumwwlk  27761  clwlkclwwlklem2a  27783  clwlkclwwlklem1  27784  clwlkclwwlkfo  27794  eupth2  28024  frgr3vlem1  28058  3vfriswmgrlem  28062  3vfriswmgr  28063  wlkl0  28152  numclwlk2lem2f1o  28164  isplig  28259  isnvlem  28393  nvi  28397  nmoubi  28555  nmounbi  28559  nmblolbi  28583  ipasslem1  28614  ipassi  28624  hlim2  28975  pjhth  29176  spansni  29340  elspansn2  29350  pjige0  29474  pjcjt2  29475  pjopyth  29503  elcnop  29640  elcnfn  29665  nmopub  29691  cnopc  29696  nmfnleub  29708  elnlfn  29711  cnfnc  29713  nmbdoplb  29808  nmcexi  29809  nmcoplb  29813  lnfnmul  29831  nmbdfnlb  29833  nmcfnlb  29837  pjss2coi  29947  pjssmi  29948  isst  29996  ishst  29997  stcltr1i  30057  mdbr  30077  dmdbr  30082  mddmd2  30092  mdslmd1lem3  30110  mdslmd1lem4  30111  elat2  30123  atcvat2  30172  cdj1i  30216  iuninc  30324  fmptcof2  30420  nn0min  30562  wrdt2ind  30653  ismnt  30691  xrge0tsmsd  30742  isomnd  30752  omndadd  30757  cyc3genpm  30844  isarchi2  30864  archirng  30867  archiexdiv  30869  archiabl  30877  isorng  30923  ofldchr  30938  mxidlval  31041  crefeq  31198  nexple  31378  esumfzf  31438  issiga  31481  isrnsiga  31482  isldsys  31525  ismeas  31568  isrnmeas  31569  measiun  31587  eulerpartlemn  31749  sseqp1  31763  rrvsum  31822  signsply0  31931  signstfvc  31954  bnj941  32154  bnj106  32250  bnj155  32261  bnj590  32292  bnj591  32293  bnj849  32307  bnj893  32310  bnj944  32320  bnj1128  32372  subfacp1lem6  32545  erdszelem8  32558  issconn  32586  cvmliftlem7  32651  cvmliftlem10  32654  cvmlift3lem2  32680  satfsschain  32724  satfrel  32727  satfdm  32729  satfrnmapom  32730  fmlafvel  32745  satffun  32769  mrsubvrs  32882  mclsssvlem  32922  mclsval  32923  mclsax  32929  mclsind  32930  shftvalg  33076  bccolsum  33084  iprodefisumlem  33085  faclimlem1  33088  dfpo2  33104  rdgprc  33152  trpredmintr  33183  frmin  33197  soseq  33209  frr3g  33234  fpr3g  33235  frrlem12  33247  fpr2  33253  frr2  33258  nosupno  33316  nosupdm  33317  nosupfv  33319  nosupres  33320  nosupbnd1lem1  33321  nosupbnd1lem3  33323  nosupbnd1lem5  33325  noeta  33335  fveleq  33912  unblimceq0  33959  bj-ax12  34103  bj-bm1.3ii  34481  rdgeqoa  34787  finxpreclem6  34813  domalom  34821  ralssiun  34824  wl-sblimt  34952  wl-sbhbt  34955  wl-2sb6d  34959  wl-mo2df  34971  wl-mo2t  34976  poimirlem2  35059  poimirlem25  35082  poimirlem28  35085  poimirlem31  35088  heicant  35092  mbfresfi  35103  itg2gt0cn  35112  sdclem2  35180  fdc  35183  seqpo  35185  incsequz  35186  mettrifi  35195  prdsbnd2  35233  heiborlem4  35252  bfplem1  35260  iscringd  35436  maxidlval  35477  igenval2  35504  iss2  35761  elrefrels3  35918  ax12eq  36237  ax12el  36238  ax12indalem  36241  ax12inda2ALT  36242  ax12inda  36244  ax12v2-o  36245  riotasvd  36252  isopos  36476  isat3  36603  ishlat1  36648  glbconN  36673  ispsubsp  37041  isldil  37406  isltrn  37415  isdilN  37450  trlval  37458  cdleme27b  37664  cdleme29b  37671  cdleme31sn1  37677  cdleme31sn1c  37684  cdleme40v  37765  cdlemk36  38209  cdlemkid5  38231  cdlemn11pre  38506  dihord2pre  38521  islpolN  38779  hdmapffval  39122  hdmapfval  39123  hdmapval2lem  39127  fzindd  39263  uzindd  39264  nnaddcom  39469  nnadddir  39471  nnmulcom  39473  ismrc  39642  incssnn0  39652  mzpexpmpt  39686  pell14qrexpclnn0  39807  monotuz  39882  rmxypos  39888  jm2.17a  39901  jm2.17b  39902  rmygeid  39905  jm2.18  39929  jm2.19lem3  39932  jm2.25  39940  jm2.15nn0  39944  jm2.16nn0  39945  wepwsolem  39986  aomclem8  40005  dfac11  40006  pwslnm  40038  lnr2i  40060  hbtlem5  40072  cnsrexpcl  40109  rngunsnply  40117  isdomn3  40148  ifpbi23  40181  elmapintrab  40276  elmapintab  40296  cnvcnvintabd  40300  eliunov2  40380  relexpxpnnidm  40404  relexpiidm  40405  relexpss1d  40406  iunrelexpmin1  40409  relexpmulnn  40410  iunrelexpmin2  40413  relexp0a  40417  trclimalb2  40427  clsk3nimkb  40743  ntrclsiso  40770  ntrclskb  40772  ntrneiiso  40794  ntrneix2  40796  ntrneixb  40798  gneispace2  40835  gneispacess2  40849  mnuunid  40985  dvgrat  41016  pm14.122b  41127  fnchoice  41658  fiiuncl  41699  ssinc  41723  ssdec  41724  wessf1ornlem  41811  dmrelrnrel  41856  fperiodmullem  41935  monoordxrv  42121  fmul01  42222  fmuldfeq  42225  climsuselem1  42249  climinff  42253  ellimcabssub0  42259  limcleqr  42286  addlimc  42290  0ellimcdiv  42291  limclner  42293  limsupref  42327  limsupub  42346  limsupmnf  42363  limsupre2lem  42366  limsupre2  42367  limsupre2mpt  42372  limsupre3lem  42374  limsupre3  42375  limsupre3mpt  42376  xlimbr  42469  cnrefiisplem  42471  dvnmptdivc  42580  dvnmptconst  42583  dvnmul  42585  iblspltprt  42615  itgspltprt  42621  stoweidlem2  42644  stoweidlem3  42645  stoweidlem17  42659  stoweidlem19  42661  stoweidlem21  42663  stoweidlem26  42668  fourierdlem42  42791  issal  42956  ismea  43090  isome  43133  carageniuncllem1  43160  caratheodorylem1  43165  2reu8i  43669  2reuimp0  43670  funressndmafv2rn  43779  2ffzoeq  43885  smonoord  43888  fargshiftf1  43958  ichnfimlem  43980  paireqne  44028  reupr  44039  reuopreuprim  44043  perfectALTVlem2  44240  lmodvsmdi  44784  dmatALTval  44809  dmatALTbasel  44811  snlindsntor  44880  ldepsnlinc  44917  elbigo2r  44967  elbigolo1  44971  itcovalt2  45091  setrecseq  45215  setrec2fun  45222  setrec2lem2  45224