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 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  345  imbi2  349  pm5.42  544  orbi2d  913  19.23t  2204  axc14  2464  mojust  2540  mof  2564  eu6lem  2574  nfabdwOLD  2932  2gencl  3473  3gencl  3474  vtocl2gf  3509  vtocl3gf  3510  vtocl2g  3511  vtocl3g  3512  vtocl2ga  3515  vtocl4g  3520  eqeu  3642  mo2icl  3650  euind  3660  reu7  3668  reuind  3689  sbctt  3793  reu8nf  3811  sbcnestgfw  4353  sbcnestgf  4358  r19.36zv  4438  dedth2h  4519  dedth3h  4520  dedth4h  4521  reusngf  4609  reuprg0  4639  preq12bg  4785  elint  4886  elintrabg  4893  intab  4910  axrep1  5211  axreplem  5212  axrep2  5213  axrep6g  5218  bm1.3ii  5227  reusv3  5329  poclOLD  5512  swopolem  5514  solin  5529  freq1  5560  frminex  5570  vtoclr  5651  2optocl  5683  3optocl  5684  raliunxp  5751  resieq  5905  iss  5946  cnveqb  6104  reu3op  6199  reuop  6200  dfpo2  6203  preddowncl  6239  funmoOLD  6457  funimaexgOLD  6528  fnbrfvb  6831  fvelimab  6850  fvmptss  6896  fmptco  7010  fprg  7036  fnressn  7039  fressnfv  7041  isoselem  7221  ovg  7446  caovcan  7485  caovordig  7486  caovord  7492  tfisi  7714  tfindsg  7716  tfinds2  7719  tfinds3  7720  dfom2  7723  elom  7724  findsg  7755  finds2  7756  f1o2ndf1  7972  poxp  7978  fnse  7983  fpr3g  8110  frrlem12  8122  fpr2a  8127  wfr3g  8147  wfrlem4OLD  8152  smoeq  8190  smores  8192  smogt  8207  tfrlem1  8216  tfr3  8239  oaordi  8386  oeordi  8427  oeoa  8437  oeoe  8439  nnacl  8451  nnmcl  8452  nnecl  8453  nnacom  8457  nnaordi  8458  nnawordi  8461  nnaass  8462  nndi  8463  nnmass  8464  nnmsucr  8465  nnmcom  8466  nnmordi  8471  2ecoptocl  8606  3ecoptocl  8607  undifixp  8731  xpdom2g  8864  findcard2  8956  unfi  8964  ssfi  8965  imafi  8967  fnfi  8973  findcard2OLD  9065  xpfi  9094  fodomfi  9101  finsschain  9135  marypha1lem  9201  marypha1  9202  supeq1  9213  ordiso2  9283  ordtypelem7  9292  wemaplem1  9314  inf3lem2  9396  inf3lem5  9399  infdiffi  9425  cantnfval2  9436  cantnfle  9438  cantnfp1lem3  9447  oemapval  9450  cantnflem1  9456  cantnf  9460  wemapwe  9464  cnfcom  9467  cnfcom3clem  9472  ttrclss  9487  ttrclselem2  9493  tz9.1  9496  frr3g  9523  frr2  9527  r1pwALT  9613  cplem2  9657  karden  9662  updjud  9701  infxpenc2lem2  9785  fseqenlem1  9789  dfac8clem  9797  alephinit  9860  dfac4  9887  dfac5lem5  9892  dfac2a  9894  dfac2b  9895  dfacacn  9906  dfac12lem3  9910  kmlem2  9916  kmlem13  9927  nnadju  9962  ackbij1lem16  10000  sornom  10042  infpssrlem4  10071  fin23lem14  10098  fin23lem32  10109  fin23lem34  10111  fin23lem36  10113  isf32lem1  10118  isf32lem2  10119  axcc2lem  10201  axcc3  10203  axcclem  10222  zornn0g  10270  ttukeylem5  10278  ttukeylem6  10279  axrepnd  10359  axpowndlem3  10364  zfcndrep  10379  fpwwe2lem7  10402  pwfseqlem3  10425  wunr1om  10484  wunfi  10486  tskr1om  10532  ingru  10580  grudomon  10582  axgroth3  10596  axgroth4  10597  nqereu  10694  mulcanenq  10725  elnp  10752  elnpi  10753  prlem934  10798  infm3  11943  nnindd  12002  nnaddcl  12005  nnmulcl  12006  nnne0  12016  peano5uzi  12418  uzind2  12422  nn0indd  12426  zindd  12430  fzindd  12431  eluzadd  12622  uzaddcl  12653  uzwo  12660  indstr  12665  zmax  12694  xmulasslem  13028  xrsupsslem  13050  xrinfmsslem  13051  xrsupss  13052  xrinfmss  13053  flval2  13543  om2uzlti  13679  uzrdgfni  13687  rabssnn0fi  13715  mptnn0fsupp  13726  seqcl2  13750  seqfveq2  13754  seqshft2  13758  monoord  13762  seqsplit  13765  seqcaopr3  13767  seqf1olem2a  13770  seqf1o  13773  seqid2  13778  seqhomo  13779  ser1const  13788  expcllem  13802  expeq0  13822  mulexp  13831  expadd  13834  expmul  13837  expmordi  13894  leexp2r  13901  leexp1a  13902  bernneq  13953  modexp  13962  facdiv  14010  faclbnd  14013  faclbnd4lem4  14019  hashgadd  14101  hashxp  14158  hashmap  14159  hashf1lem2  14179  hashf1  14180  seqcoll  14187  wrdind  14444  wrd2ind  14445  pfxccatin12lem3  14454  cshweqrep  14543  2cshwcshw  14547  relexp0g  14742  relexpsucnnr  14745  relexpsucnnl  14750  relexpcnv  14755  relexpnndm  14761  relexpaddnn  14771  rtrclreclem1  14777  dfrtrclrec2  14778  rtrclreclem2  14779  rtrclreclem4  14781  dfrtrcl2  14782  relexpind  14784  reusq0  15183  rlim  15213  rlim2  15214  rlim0  15226  rlim0lt  15227  rlimi  15231  ello12r  15235  ello1mpt  15239  ello1d  15241  elo12r  15246  lo1o1  15250  o1lo1  15255  lo1res  15277  climshft  15294  o1compt  15305  rlimo1  15335  lo1add  15345  lo1mul  15346  rlimdiv  15366  climub  15382  climserle  15383  caucvgrlem  15393  caurcvgr  15394  iseraltlem2  15403  summolem2a  15436  sumss  15445  fsum2d  15492  fsumabs  15522  fsumrlim  15532  fsumo1  15533  fsumiun  15542  binom  15551  climcndslem1  15570  climcndslem2  15571  cvgrat  15604  clim2prod  15609  prodfn0  15615  prodfrec  15616  ntrivcvgfvn0  15620  prodmolem2a  15653  fprodabs  15693  fprodn0  15698  fprod2d  15700  binomfallfac  15760  bpolycl  15771  bpolydif  15774  fprodefsum  15813  demoivreALT  15919  ruclem8  15955  ruclem9  15956  dvdsle  16028  dvdsfac  16044  divalglem7  16117  bitsinv1  16158  sadcadd  16174  sadadd2  16176  saddisjlem  16180  smuval2  16198  smupvallem  16199  smu01lem  16201  smupval  16204  smueqlem  16206  smumullem  16208  bezoutlem4  16259  dfgcd2  16263  gcdmultipleOLD  16269  rplpwr  16276  nn0seqcvgd  16284  seq1st  16285  alginv  16289  algcvga  16293  algfx  16294  lcmf  16347  prmind2  16399  prmdvdsexp  16429  prmfac1  16435  reumodprminv  16514  pcmpt  16602  pcfac  16609  prmpwdvds  16614  prmreclem4  16629  vdwlem10  16700  ramval  16718  ramcl  16739  cshwrepswhash1  16813  prmlem1a  16817  imasleval  17261  ismre  17308  mreexexd  17366  lubprop  18085  lublecllem  18087  glbprop  18098  joinlem  18110  meetlem  18124  poslubmo  18138  posglbmo  18139  poslubd  18140  isglbd  18236  lubun  18242  mndind  18475  frmdgsum  18510  mulgnnass  18747  mhmmulg  18753  gsumwrev  18982  gsmsymgrfix  19045  gsmsymgreq  19049  psgnunilem3  19113  sylow1lem1  19212  efginvrel2  19342  efgsrel  19349  efgredlemd  19359  efgredlem  19362  efgred  19363  efgrelexlemb  19365  gsum2dlem2  19581  gsumcom2  19585  ablfac1eulem  19684  pgpfac1lem2  19687  pgpfac1lem5  19691  pgpfac1  19692  pgpfac  19696  srgmulgass  19776  srgpcomp  19777  srgbinom  19790  lmodvsmmulgdi  20167  isdomn2  20579  cnfldexp  20640  islindf4  21054  assamulgscm  21114  mplcoe1  21247  mplcoe3  21248  mplcoe5  21250  gsummoncoe1  21484  dmatval  21650  dmatel  21651  dmatmulcl  21658  pmatcoe1fsupp  21859  decpmataa0  21926  decpmatmulsumfsupp  21931  pmatcollpw2lem  21935  pm2mpmhmlem1  21976  fiinopn  22059  mretopd  22252  neiptoptop  22291  cnpfval  22394  iscnp3  22404  tgcn  22412  lmbr  22418  lmbr2  22419  lmbrf  22420  lmss  22458  ishaus  22482  hausnei2  22513  t1sep2  22529  fiuncmp  22564  dfconn2  22579  1stcfb  22605  2ndc1stc  22611  1stcrest  22613  1stcelcls  22621  1stccn  22623  lly1stc  22656  elkgen  22696  kgencn  22716  tx1stc  22810  xkopt  22815  cnmptcom  22838  isr0  22897  r0sep  22908  ptcmpfi  22973  isfildlem  23017  rnelfm  23113  fbflim  23136  flimrest  23143  isflf  23153  flffbas  23155  lmflf  23165  fclsrest  23184  isfcf  23194  cnextfvval  23225  tmdgsum  23255  eltsms  23293  tsmsi  23294  tsmsgsum  23299  tsmssubm  23303  tsmsres  23304  tsmsf1o  23305  isust  23364  isucn  23439  isucn2  23440  ucnima  23442  imasdsf1olem  23535  metss  23673  met1stc  23686  metcnp  23706  metcnpi  23709  metcnpi2  23710  metucn  23736  xrge0tsms  24006  fsumcn  24042  elcncf  24061  cncfi  24066  rescncf  24069  cncfco  24079  caucfil  24456  equivcau  24473  caubl  24481  caublcls  24482  ovolgelb  24653  ovolunlem1a  24669  ovolicc2lem3  24692  voliunlem1  24723  voliunlem3  24725  volsuplem  24728  volsup  24729  dyadmax  24771  vitali  24786  itg2leub  24908  itgfsum  25000  dvnadd  25102  dvnres  25104  cpnord  25108  dvnfre  25125  dvmptfsum  25148  dvferm1  25158  dvferm2  25160  rolle  25163  dvlip  25166  c1lip1  25170  lhop1  25187  deg1leb  25269  ply1divex  25310  fta1g  25341  plyco  25411  dgrcolem1  25443  dgrco  25445  dvnply2  25456  plydivex  25466  aalioulem2  25502  aalioulem3  25503  aalioulem5  25505  aaliou3lem2  25512  dvntaylp  25539  taylthlem1  25541  ulmdvlem3  25570  abelthlem9  25608  cxpmul2  25853  scvxcvx  26144  jensenlem2  26146  jensen  26147  wilthlem3  26228  perfectlem2  26387  bcmono  26434  bposlem5  26445  lgsquad2lem2  26542  addsq2reu  26597  2sqreulem1  26603  2sqreunnlem1  26606  dchrisumlem1  26646  dchrisum0flb  26667  pntpbnd1  26743  pntlemf  26762  qabvle  26782  qabvexp  26783  ostthlem2  26785  ostth2lem2  26791  tgcgr4  26901  usgr2pth  28141  wlkiswwlks2lem4  28246  wlkiswwlks2  28249  rusgrnumwwlk  28349  clwlkclwwlklem2a  28371  clwlkclwwlklem1  28372  clwlkclwwlkfo  28382  eupth2  28612  frgr3vlem1  28646  3vfriswmgrlem  28650  3vfriswmgr  28651  wlkl0  28740  numclwlk2lem2f1o  28752  isplig  28847  isnvlem  28981  nvi  28985  nmoubi  29143  nmounbi  29147  nmblolbi  29171  ipasslem1  29202  ipassi  29212  hlim2  29563  pjhth  29764  spansni  29928  elspansn2  29938  pjige0  30062  pjcjt2  30063  pjopyth  30091  elcnop  30228  elcnfn  30253  nmopub  30279  cnopc  30284  nmfnleub  30296  elnlfn  30299  cnfnc  30301  nmbdoplb  30396  nmcexi  30397  nmcoplb  30401  lnfnmul  30419  nmbdfnlb  30421  nmcfnlb  30425  pjss2coi  30535  pjssmi  30536  isst  30584  ishst  30585  stcltr1i  30645  mdbr  30665  dmdbr  30670  mddmd2  30680  mdslmd1lem3  30698  mdslmd1lem4  30699  elat2  30711  atcvat2  30760  cdj1i  30804  iuninc  30909  fmptcof2  31003  nn0min  31143  wrdt2ind  31234  ismnt  31270  xrge0tsmsd  31326  isomnd  31336  omndadd  31341  cyc3genpm  31428  isarchi2  31448  archirng  31451  archiexdiv  31453  archiabl  31461  isorng  31507  ofldchr  31522  mxidlval  31642  crefeq  31804  nexple  31986  esumfzf  32046  issiga  32089  isrnsiga  32090  isldsys  32133  ismeas  32176  isrnmeas  32177  measiun  32195  eulerpartlemn  32357  sseqp1  32371  rrvsum  32430  signsply0  32539  signstfvc  32562  bnj941  32761  bnj106  32857  bnj155  32868  bnj590  32899  bnj591  32900  bnj849  32914  bnj893  32917  bnj944  32927  bnj1128  32979  subfacp1lem6  33156  erdszelem8  33169  issconn  33197  cvmliftlem7  33262  cvmliftlem10  33265  cvmlift3lem2  33291  satfsschain  33335  satfrel  33338  satfdm  33340  satfrnmapom  33341  fmlafvel  33356  satffun  33380  mrsubvrs  33493  mclsssvlem  33533  mclsval  33534  mclsax  33540  mclsind  33541  shftvalg  33706  bccolsum  33714  iprodefisumlem  33715  faclimlem1  33718  rdgprc  33779  soseq  33812  naddssim  33846  nosupcbv  33914  nosupno  33915  nosupdm  33916  nosupfv  33918  nosupres  33919  nosupbnd1lem1  33920  nosupbnd1lem3  33922  nosupbnd1lem5  33924  noinfcbv  33929  noinfno  33930  noinfdm  33931  noinffv  33933  noinfres  33934  noinfbnd1lem3  33937  noinfbnd1lem5  33939  eqscut2  34009  fveleq  34649  unblimceq0  34696  bj-ax12  34847  bj-bm1.3ii  35244  rdgeqoa  35550  finxpreclem6  35576  domalom  35584  ralssiun  35587  wl-sblimt  35715  wl-sbhbt  35718  wl-2sb6d  35722  wl-mo2df  35734  wl-mo2t  35739  poimirlem2  35788  poimirlem25  35811  poimirlem28  35814  poimirlem31  35817  heicant  35821  mbfresfi  35832  itg2gt0cn  35841  sdclem2  35909  fdc  35912  seqpo  35914  incsequz  35915  mettrifi  35924  prdsbnd2  35962  heiborlem4  35981  bfplem1  35989  iscringd  36165  maxidlval  36206  igenval2  36233  iss2  36486  elrefrels3  36643  ax12eq  36962  ax12el  36963  ax12indalem  36966  ax12inda2ALT  36967  ax12inda  36969  ax12v2-o  36970  riotasvd  36977  isopos  37201  isat3  37328  ishlat1  37373  glbconN  37398  ispsubsp  37766  isldil  38131  isltrn  38140  isdilN  38175  trlval  38183  cdleme27b  38389  cdleme29b  38396  cdleme31sn1  38402  cdleme31sn1c  38409  cdleme40v  38490  cdlemk36  38934  cdlemkid5  38956  cdlemn11pre  39231  dihord2pre  39246  islpolN  39504  hdmapffval  39847  hdmapfval  39848  hdmapval2lem  39852  uzindd  39992  sticksstones1  40109  sticksstones2  40110  sticksstones3  40111  sticksstones8  40116  sticksstones10  40118  sticksstones11  40119  sticksstones12a  40120  sticksstones15  40124  nnaddcom  40305  nnadddir  40307  nnmulcom  40309  ismrc  40530  incssnn0  40540  mzpexpmpt  40574  pell14qrexpclnn0  40695  monotuz  40770  rmxypos  40776  jm2.17a  40789  jm2.17b  40790  rmygeid  40793  jm2.18  40817  jm2.19lem3  40820  jm2.25  40828  jm2.15nn0  40832  jm2.16nn0  40833  wepwsolem  40874  aomclem8  40893  dfac11  40894  pwslnm  40926  lnr2i  40948  hbtlem5  40960  cnsrexpcl  40997  rngunsnply  41005  isdomn3  41036  ifpbi23  41087  elmapintrab  41191  elmapintab  41211  cnvcnvintabd  41215  eliunov2  41294  relexpxpnnidm  41318  relexpiidm  41319  relexpss1d  41320  iunrelexpmin1  41323  relexpmulnn  41324  iunrelexpmin2  41327  relexp0a  41331  trclimalb2  41341  clsk3nimkb  41657  ntrclsiso  41684  ntrclskb  41686  ntrneiiso  41708  ntrneix2  41710  ntrneixb  41712  gneispace2  41749  gneispacess2  41763  mnuunid  41902  dvgrat  41937  pm14.122b  42048  fnchoice  42579  fiiuncl  42620  ssinc  42644  ssdec  42645  wessf1ornlem  42729  dmrelrnrel  42772  fperiodmullem  42849  monoordxrv  43029  fmul01  43128  fmuldfeq  43131  climsuselem1  43155  climinff  43159  ellimcabssub0  43165  limcleqr  43192  addlimc  43196  0ellimcdiv  43197  limclner  43199  limsupref  43233  limsupub  43252  limsupmnf  43269  limsupre2lem  43272  limsupre2  43273  limsupre2mpt  43278  limsupre3lem  43280  limsupre3  43281  limsupre3mpt  43282  xlimbr  43375  cnrefiisplem  43377  dvnmptdivc  43486  dvnmptconst  43489  dvnmul  43491  iblspltprt  43521  itgspltprt  43527  stoweidlem2  43550  stoweidlem3  43551  stoweidlem17  43565  stoweidlem19  43567  stoweidlem21  43569  stoweidlem26  43574  fourierdlem42  43697  issal  43862  ismea  43996  isome  44039  carageniuncllem1  44066  caratheodorylem1  44071  2reu8i  44616  2reuimp0  44617  funressndmafv2rn  44726  2ffzoeq  44831  smonoord  44834  fargshiftf1  44904  ichnfimlem  44926  paireqne  44974  reupr  44985  reuopreuprim  44989  perfectALTVlem2  45185  lmodvsmdi  45729  dmatALTval  45752  dmatALTbasel  45754  snlindsntor  45823  ldepsnlinc  45860  elbigo2r  45910  elbigolo1  45914  itcovalt2  46034  mof0  46176  isnrm4  46235  iscnrm3r  46253  iscnrm4  46259  lubsscl  46265  glbsscl  46266  ipolubdm  46284  ipoglbdm  46287  setrecseq  46402  setrec2fun  46409  setrec2lem2  46411