Theorem imbi2d 340

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  344  imbi2  348  pm5.42  543  orbi2d  912  19.23t  2206  axc14  2463  mojust  2539  mof  2563  eu6lem  2573  nfabdwOLD  2930  2gencl  3462  3gencl  3463  vtocl2gf  3498  vtocl3gf  3499  vtocl2g  3500  vtocl3g  3501  vtocl2ga  3504  vtocl4g  3509  eqeu  3636  mo2icl  3644  euind  3654  reu7  3662  reuind  3683  sbctt  3788  reu8nf  3806  sbcnestgfw  4349  sbcnestgf  4354  r19.36zv  4434  dedth2h  4515  dedth3h  4516  dedth4h  4517  reusngf  4605  reuprg0  4635  preq12bg  4781  elint  4882  elintrabg  4889  intab  4906  axrep1  5206  axreplem  5207  axrep2  5208  bm1.3ii  5221  reusv3  5323  poclOLD  5502  swopolem  5504  solin  5519  freq1  5550  frminex  5560  vtoclr  5641  2optocl  5672  3optocl  5673  raliunxp  5737  resieq  5891  iss  5932  cnveqb  6088  reu3op  6184  reuop  6185  dfpo2  6188  preddowncl  6224  funmo  6434  funimaexg  6504  fnbrfvb  6804  fvelimab  6823  fvmptss  6869  fmptco  6983  fprg  7009  fnressn  7012  fressnfv  7014  isoselem  7192  ovg  7415  caovcan  7454  caovordig  7455  caovord  7461  tfisi  7680  tfindsg  7682  tfinds2  7685  tfinds3  7686  dfom2  7689  elom  7690  findsg  7720  finds2  7721  f1o2ndf1  7934  poxp  7940  fnse  7945  fpr3g  8072  frrlem12  8084  fpr2a  8089  wfr3g  8109  wfrlem4OLD  8114  smoeq  8152  smores  8154  smogt  8169  tfrlem1  8178  tfr3  8201  oaordi  8339  oeordi  8380  oeoa  8390  oeoe  8392  nnacl  8404  nnmcl  8405  nnecl  8406  nnacom  8410  nnaordi  8411  nnawordi  8414  nnaass  8415  nndi  8416  nnmass  8417  nnmsucr  8418  nnmcom  8419  nnmordi  8424  2ecoptocl  8555  3ecoptocl  8556  undifixp  8680  xpdom2g  8808  findcard2  8909  unfi  8917  ssfi  8918  imafi  8920  fnfi  8925  findcard2OLD  8986  xpfi  9015  fodomfi  9022  finsschain  9056  marypha1lem  9122  marypha1  9123  supeq1  9134  ordiso2  9204  ordtypelem7  9213  wemaplem1  9235  inf3lem2  9317  inf3lem5  9320  infdiffi  9346  cantnfval2  9357  cantnfle  9359  cantnfp1lem3  9368  oemapval  9371  cantnflem1  9377  cantnf  9381  wemapwe  9385  cnfcom  9388  cnfcom3clem  9393  trpredmintr  9409  tz9.1  9418  frmin  9438  frr3g  9445  frr2  9449  r1pwALT  9535  cplem2  9579  karden  9584  updjud  9623  infxpenc2lem2  9707  fseqenlem1  9711  dfac8clem  9719  alephinit  9782  dfac4  9809  dfac5lem5  9814  dfac2a  9816  dfac2b  9817  dfacacn  9828  dfac12lem3  9832  kmlem2  9838  kmlem13  9849  nnadju  9884  ackbij1lem16  9922  sornom  9964  infpssrlem4  9993  fin23lem14  10020  fin23lem32  10031  fin23lem34  10033  fin23lem36  10035  isf32lem1  10040  isf32lem2  10041  axcc2lem  10123  axcc3  10125  axcclem  10144  zornn0g  10192  ttukeylem5  10200  ttukeylem6  10201  axrepnd  10281  axpowndlem3  10286  zfcndrep  10301  fpwwe2lem7  10324  pwfseqlem3  10347  wunr1om  10406  wunfi  10408  tskr1om  10454  ingru  10502  grudomon  10504  axgroth3  10518  axgroth4  10519  nqereu  10616  mulcanenq  10647  elnp  10674  elnpi  10675  prlem934  10720  infm3  11864  nnindd  11923  nnaddcl  11926  nnmulcl  11927  nnne0  11937  peano5uzi  12339  uzind2  12343  nn0indd  12347  zindd  12351  eluzadd  12542  uzaddcl  12573  uzwo  12580  indstr  12585  zmax  12614  xmulasslem  12948  xrsupsslem  12970  xrinfmsslem  12971  xrsupss  12972  xrinfmss  12973  flval2  13462  om2uzlti  13598  uzrdgfni  13606  rabssnn0fi  13634  mptnn0fsupp  13645  seqcl2  13669  seqfveq2  13673  seqshft2  13677  monoord  13681  seqsplit  13684  seqcaopr3  13686  seqf1olem2a  13689  seqf1o  13692  seqid2  13697  seqhomo  13698  ser1const  13707  expcllem  13721  expeq0  13741  mulexp  13750  expadd  13753  expmul  13756  expmordi  13813  leexp2r  13820  leexp1a  13821  bernneq  13872  modexp  13881  facdiv  13929  faclbnd  13932  faclbnd4lem4  13938  hashgadd  14020  hashxp  14077  hashmap  14078  hashf1lem2  14098  hashf1  14099  seqcoll  14106  wrdind  14363  wrd2ind  14364  pfxccatin12lem3  14373  cshweqrep  14462  2cshwcshw  14466  relexp0g  14661  relexpsucnnr  14664  relexpsucnnl  14669  relexpcnv  14674  relexpnndm  14680  relexpaddnn  14690  rtrclreclem1  14696  dfrtrclrec2  14697  rtrclreclem2  14698  rtrclreclem4  14700  dfrtrcl2  14701  relexpind  14703  reusq0  15102  rlim  15132  rlim2  15133  rlim0  15145  rlim0lt  15146  rlimi  15150  ello12r  15154  ello1mpt  15158  ello1d  15160  elo12r  15165  lo1o1  15169  o1lo1  15174  lo1res  15196  climshft  15213  o1compt  15224  rlimo1  15254  lo1add  15264  lo1mul  15265  rlimdiv  15285  climub  15301  climserle  15302  caucvgrlem  15312  caurcvgr  15313  iseraltlem2  15322  summolem2a  15355  sumss  15364  fsum2d  15411  fsumabs  15441  fsumrlim  15451  fsumo1  15452  fsumiun  15461  binom  15470  climcndslem1  15489  climcndslem2  15490  cvgrat  15523  clim2prod  15528  prodfn0  15534  prodfrec  15535  ntrivcvgfvn0  15539  prodmolem2a  15572  fprodabs  15612  fprodn0  15617  fprod2d  15619  binomfallfac  15679  bpolycl  15690  bpolydif  15693  fprodefsum  15732  demoivreALT  15838  ruclem8  15874  ruclem9  15875  dvdsle  15947  dvdsfac  15963  divalglem7  16036  bitsinv1  16077  sadcadd  16093  sadadd2  16095  saddisjlem  16099  smuval2  16117  smupvallem  16118  smu01lem  16120  smupval  16123  smueqlem  16125  smumullem  16127  bezoutlem4  16178  dfgcd2  16182  gcdmultipleOLD  16188  rplpwr  16195  nn0seqcvgd  16203  seq1st  16204  alginv  16208  algcvga  16212  algfx  16213  lcmf  16266  prmind2  16318  prmdvdsexp  16348  prmfac1  16354  reumodprminv  16433  pcmpt  16521  pcfac  16528  prmpwdvds  16533  prmreclem4  16548  vdwlem10  16619  ramval  16637  ramcl  16658  cshwrepswhash1  16732  prmlem1a  16736  imasleval  17169  ismre  17216  mreexexd  17274  lubprop  17991  lublecllem  17993  glbprop  18004  joinlem  18016  meetlem  18030  poslubmo  18044  posglbmo  18045  poslubd  18046  isglbd  18142  lubun  18148  mndind  18381  frmdgsum  18416  mulgnnass  18653  mhmmulg  18659  gsumwrev  18888  gsmsymgrfix  18951  gsmsymgreq  18955  psgnunilem3  19019  sylow1lem1  19118  efginvrel2  19248  efgsrel  19255  efgredlemd  19265  efgredlem  19268  efgred  19269  efgrelexlemb  19271  gsum2dlem2  19487  gsumcom2  19491  ablfac1eulem  19590  pgpfac1lem2  19593  pgpfac1lem5  19597  pgpfac1  19598  pgpfac  19602  srgmulgass  19682  srgpcomp  19683  srgbinom  19696  lmodvsmmulgdi  20073  isdomn2  20483  cnfldexp  20543  islindf4  20955  assamulgscm  21015  mplcoe1  21148  mplcoe3  21149  mplcoe5  21151  gsummoncoe1  21385  dmatval  21549  dmatel  21550  dmatmulcl  21557  pmatcoe1fsupp  21758  decpmataa0  21825  decpmatmulsumfsupp  21830  pmatcollpw2lem  21834  pm2mpmhmlem1  21875  fiinopn  21958  mretopd  22151  neiptoptop  22190  cnpfval  22293  iscnp3  22303  tgcn  22311  lmbr  22317  lmbr2  22318  lmbrf  22319  lmss  22357  ishaus  22381  hausnei2  22412  t1sep2  22428  fiuncmp  22463  dfconn2  22478  1stcfb  22504  2ndc1stc  22510  1stcrest  22512  1stcelcls  22520  1stccn  22522  lly1stc  22555  elkgen  22595  kgencn  22615  tx1stc  22709  xkopt  22714  cnmptcom  22737  isr0  22796  r0sep  22807  ptcmpfi  22872  isfildlem  22916  rnelfm  23012  fbflim  23035  flimrest  23042  isflf  23052  flffbas  23054  lmflf  23064  fclsrest  23083  isfcf  23093  cnextfvval  23124  tmdgsum  23154  eltsms  23192  tsmsi  23193  tsmsgsum  23198  tsmssubm  23202  tsmsres  23203  tsmsf1o  23204  isust  23263  isucn  23338  isucn2  23339  ucnima  23341  imasdsf1olem  23434  metss  23570  met1stc  23583  metcnp  23603  metcnpi  23606  metcnpi2  23607  metucn  23633  xrge0tsms  23903  fsumcn  23939  elcncf  23958  cncfi  23963  rescncf  23966  cncfco  23976  caucfil  24352  equivcau  24369  caubl  24377  caublcls  24378  ovolgelb  24549  ovolunlem1a  24565  ovolicc2lem3  24588  voliunlem1  24619  voliunlem3  24621  volsuplem  24624  volsup  24625  dyadmax  24667  vitali  24682  itg2leub  24804  itgfsum  24896  dvnadd  24998  dvnres  25000  cpnord  25004  dvnfre  25021  dvmptfsum  25044  dvferm1  25054  dvferm2  25056  rolle  25059  dvlip  25062  c1lip1  25066  lhop1  25083  deg1leb  25165  ply1divex  25206  fta1g  25237  plyco  25307  dgrcolem1  25339  dgrco  25341  dvnply2  25352  plydivex  25362  aalioulem2  25398  aalioulem3  25399  aalioulem5  25401  aaliou3lem2  25408  dvntaylp  25435  taylthlem1  25437  ulmdvlem3  25466  abelthlem9  25504  cxpmul2  25749  scvxcvx  26040  jensenlem2  26042  jensen  26043  wilthlem3  26124  perfectlem2  26283  bcmono  26330  bposlem5  26341  lgsquad2lem2  26438  addsq2reu  26493  2sqreulem1  26499  2sqreunnlem1  26502  dchrisumlem1  26542  dchrisum0flb  26563  pntpbnd1  26639  pntlemf  26658  qabvle  26678  qabvexp  26679  ostthlem2  26681  ostth2lem2  26687  tgcgr4  26796  usgr2pth  28033  wlkiswwlks2lem4  28138  wlkiswwlks2  28141  rusgrnumwwlk  28241  clwlkclwwlklem2a  28263  clwlkclwwlklem1  28264  clwlkclwwlkfo  28274  eupth2  28504  frgr3vlem1  28538  3vfriswmgrlem  28542  3vfriswmgr  28543  wlkl0  28632  numclwlk2lem2f1o  28644  isplig  28739  isnvlem  28873  nvi  28877  nmoubi  29035  nmounbi  29039  nmblolbi  29063  ipasslem1  29094  ipassi  29104  hlim2  29455  pjhth  29656  spansni  29820  elspansn2  29830  pjige0  29954  pjcjt2  29955  pjopyth  29983  elcnop  30120  elcnfn  30145  nmopub  30171  cnopc  30176  nmfnleub  30188  elnlfn  30191  cnfnc  30193  nmbdoplb  30288  nmcexi  30289  nmcoplb  30293  lnfnmul  30311  nmbdfnlb  30313  nmcfnlb  30317  pjss2coi  30427  pjssmi  30428  isst  30476  ishst  30477  stcltr1i  30537  mdbr  30557  dmdbr  30562  mddmd2  30572  mdslmd1lem3  30590  mdslmd1lem4  30591  elat2  30603  atcvat2  30652  cdj1i  30696  iuninc  30801  fmptcof2  30896  nn0min  31036  wrdt2ind  31127  ismnt  31163  xrge0tsmsd  31219  isomnd  31229  omndadd  31234  cyc3genpm  31321  isarchi2  31341  archirng  31344  archiexdiv  31346  archiabl  31354  isorng  31400  ofldchr  31415  mxidlval  31535  crefeq  31697  nexple  31877  esumfzf  31937  issiga  31980  isrnsiga  31981  isldsys  32024  ismeas  32067  isrnmeas  32068  measiun  32086  eulerpartlemn  32248  sseqp1  32262  rrvsum  32321  signsply0  32430  signstfvc  32453  bnj941  32652  bnj106  32748  bnj155  32759  bnj590  32790  bnj591  32791  bnj849  32805  bnj893  32808  bnj944  32818  bnj1128  32870  subfacp1lem6  33047  erdszelem8  33060  issconn  33088  cvmliftlem7  33153  cvmliftlem10  33156  cvmlift3lem2  33182  satfsschain  33226  satfrel  33229  satfdm  33231  satfrnmapom  33232  fmlafvel  33247  satffun  33271  mrsubvrs  33384  mclsssvlem  33424  mclsval  33425  mclsax  33431  mclsind  33432  shftvalg  33603  bccolsum  33611  iprodefisumlem  33612  faclimlem1  33615  rdgprc  33676  ttrclss  33706  ttrclselem2  33712  soseq  33730  naddssim  33764  nosupcbv  33832  nosupno  33833  nosupdm  33834  nosupfv  33836  nosupres  33837  nosupbnd1lem1  33838  nosupbnd1lem3  33840  nosupbnd1lem5  33842  noinfcbv  33847  noinfno  33848  noinfdm  33849  noinffv  33851  noinfres  33852  noinfbnd1lem3  33855  noinfbnd1lem5  33857  eqscut2  33927  fveleq  34567  unblimceq0  34614  bj-ax12  34765  bj-bm1.3ii  35162  rdgeqoa  35468  finxpreclem6  35494  domalom  35502  ralssiun  35505  wl-sblimt  35633  wl-sbhbt  35636  wl-2sb6d  35640  wl-mo2df  35652  wl-mo2t  35657  poimirlem2  35706  poimirlem25  35729  poimirlem28  35732  poimirlem31  35735  heicant  35739  mbfresfi  35750  itg2gt0cn  35759  sdclem2  35827  fdc  35830  seqpo  35832  incsequz  35833  mettrifi  35842  prdsbnd2  35880  heiborlem4  35899  bfplem1  35907  iscringd  36083  maxidlval  36124  igenval2  36151  iss2  36406  elrefrels3  36563  ax12eq  36882  ax12el  36883  ax12indalem  36886  ax12inda2ALT  36887  ax12inda  36889  ax12v2-o  36890  riotasvd  36897  isopos  37121  isat3  37248  ishlat1  37293  glbconN  37318  ispsubsp  37686  isldil  38051  isltrn  38060  isdilN  38095  trlval  38103  cdleme27b  38309  cdleme29b  38316  cdleme31sn1  38322  cdleme31sn1c  38329  cdleme40v  38410  cdlemk36  38854  cdlemkid5  38876  cdlemn11pre  39151  dihord2pre  39166  islpolN  39424  hdmapffval  39767  hdmapfval  39768  hdmapval2lem  39772  fzindd  39912  uzindd  39913  sticksstones1  40030  sticksstones2  40031  sticksstones3  40032  sticksstones8  40037  sticksstones10  40039  sticksstones11  40040  sticksstones12a  40041  sticksstones15  40045  nnaddcom  40219  nnadddir  40221  nnmulcom  40223  ismrc  40439  incssnn0  40449  mzpexpmpt  40483  pell14qrexpclnn0  40604  monotuz  40679  rmxypos  40685  jm2.17a  40698  jm2.17b  40699  rmygeid  40702  jm2.18  40726  jm2.19lem3  40729  jm2.25  40737  jm2.15nn0  40741  jm2.16nn0  40742  wepwsolem  40783  aomclem8  40802  dfac11  40803  pwslnm  40835  lnr2i  40857  hbtlem5  40869  cnsrexpcl  40906  rngunsnply  40914  isdomn3  40945  ifpbi23  40978  elmapintrab  41073  elmapintab  41093  cnvcnvintabd  41097  eliunov2  41176  relexpxpnnidm  41200  relexpiidm  41201  relexpss1d  41202  iunrelexpmin1  41205  relexpmulnn  41206  iunrelexpmin2  41209  relexp0a  41213  trclimalb2  41223  clsk3nimkb  41539  ntrclsiso  41566  ntrclskb  41568  ntrneiiso  41590  ntrneix2  41592  ntrneixb  41594  gneispace2  41631  gneispacess2  41645  mnuunid  41784  dvgrat  41819  pm14.122b  41930  fnchoice  42461  fiiuncl  42502  ssinc  42526  ssdec  42527  wessf1ornlem  42611  dmrelrnrel  42654  fperiodmullem  42732  monoordxrv  42912  fmul01  43011  fmuldfeq  43014  climsuselem1  43038  climinff  43042  ellimcabssub0  43048  limcleqr  43075  addlimc  43079  0ellimcdiv  43080  limclner  43082  limsupref  43116  limsupub  43135  limsupmnf  43152  limsupre2lem  43155  limsupre2  43156  limsupre2mpt  43161  limsupre3lem  43163  limsupre3  43164  limsupre3mpt  43165  xlimbr  43258  cnrefiisplem  43260  dvnmptdivc  43369  dvnmptconst  43372  dvnmul  43374  iblspltprt  43404  itgspltprt  43410  stoweidlem2  43433  stoweidlem3  43434  stoweidlem17  43448  stoweidlem19  43450  stoweidlem21  43452  stoweidlem26  43457  fourierdlem42  43580  issal  43745  ismea  43879  isome  43922  carageniuncllem1  43949  caratheodorylem1  43954  2reu8i  44492  2reuimp0  44493  funressndmafv2rn  44602  2ffzoeq  44708  smonoord  44711  fargshiftf1  44781  ichnfimlem  44803  paireqne  44851  reupr  44862  reuopreuprim  44866  perfectALTVlem2  45062  lmodvsmdi  45606  dmatALTval  45629  dmatALTbasel  45631  snlindsntor  45700  ldepsnlinc  45737  elbigo2r  45787  elbigolo1  45791  itcovalt2  45911  mof0  46053  isnrm4  46112  iscnrm3r  46130  iscnrm4  46136  lubsscl  46142  glbsscl  46143  ipolubdm  46161  ipoglbdm  46164  setrecseq  46277  setrec2fun  46284  setrec2lem2  46286