Theorem imbi2d 343

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  imbi12d  347  imbi2  351  pm5.42  546  orbi2d  912  con3ALTOLD  1081  19.23t  2210  axc14  2486  mojust  2621  mof  2647  eu6lem  2658  nfabdw  3002  2gencl  3537  3gencl  3538  vtocl2gf  3572  vtocl3gf  3573  vtocl2g  3574  vtocl2ga  3577  vtocl4g  3581  eqeu  3699  mo2icl  3707  euind  3717  reu7  3725  reuind  3746  sbctt  3846  reu8nf  3862  vtocl2dOLD  3933  sbcnestgfw  4372  sbcnestgf  4377  r19.36zv  4454  dedth2h  4526  dedth3h  4527  dedth4h  4528  reusngf  4614  reuprg0  4640  preq12bg  4786  elint  4884  elintrabg  4891  intab  4908  axrep1  5193  axreplem  5194  axrep2  5195  bm1.3ii  5208  reusv3  5308  pocl  5483  swopolem  5485  solin  5500  freq1  5527  frminex  5537  vtoclr  5617  2optocl  5648  3optocl  5649  raliunxp  5712  resieq  5866  iss  5905  cnveqb  6055  reu3op  6145  reuop  6146  preddowncl  6177  funmo  6373  funimaexg  6442  fnbrfvb  6720  fvelimab  6739  fvmptss  6782  fmptco  6893  fprg  6919  fnressn  6922  fressnfv  6924  isoselem  7096  ovg  7315  caovcan  7354  caovordig  7355  caovord  7361  tfisi  7575  tfindsg  7577  tfinds2  7580  tfinds3  7581  dfom2  7584  elom  7585  findsg  7611  finds2  7612  f1o2ndf1  7820  poxp  7824  fnse  7829  wfr3g  7955  wfrlem4  7960  smoeq  7989  smores  7991  smogt  8006  tfrlem1  8014  tfr3  8037  oaordi  8174  oeordi  8215  oeoa  8225  oeoe  8227  nnacl  8239  nnmcl  8240  nnecl  8241  nnacom  8245  nnaordi  8246  nnawordi  8249  nnaass  8250  nndi  8251  nnmass  8252  nnmsucr  8253  nnmcom  8254  nnmordi  8259  2ecoptocl  8390  3ecoptocl  8391  undifixp  8500  xpdom2g  8615  findcard2  8760  xpfi  8791  fnfi  8798  fodomfi  8799  finsschain  8833  marypha1lem  8899  marypha1  8900  supeq1  8911  ordiso2  8981  ordtypelem7  8990  wemaplem1  9012  inf3lem2  9094  inf3lem5  9097  infdiffi  9123  cantnfval2  9134  cantnfle  9136  cantnfp1lem3  9145  oemapval  9148  cantnflem1  9154  cantnf  9158  wemapwe  9162  cnfcom  9165  cnfcom3clem  9170  tz9.1  9173  r1pwALT  9277  cplem2  9321  karden  9326  updjud  9365  infxpenc2lem2  9448  fseqenlem1  9452  dfac8clem  9460  alephinit  9523  dfac4  9550  dfac5lem5  9555  dfac2a  9557  dfac2b  9558  dfacacn  9569  dfac12lem3  9573  kmlem2  9579  kmlem13  9590  ackbij1lem16  9659  sornom  9701  infpssrlem4  9730  fin23lem14  9757  fin23lem32  9768  fin23lem34  9770  fin23lem36  9772  isf32lem1  9777  isf32lem2  9778  axcc2lem  9860  axcc3  9862  axcclem  9881  zornn0g  9929  ttukeylem5  9937  ttukeylem6  9938  axrepnd  10018  axpowndlem3  10023  zfcndrep  10038  fpwwe2lem8  10061  pwfseqlem3  10084  wunr1om  10143  wunfi  10145  tskr1om  10191  ingru  10239  grudomon  10241  axgroth3  10255  axgroth4  10256  nqereu  10353  mulcanenq  10384  elnp  10411  elnpi  10412  prlem934  10457  infm3  11602  nnindd  11660  nnaddcl  11663  nnmulcl  11664  nnne0  11674  peano5uzi  12074  uzind2  12078  nn0indd  12082  zindd  12086  eluzadd  12276  uzaddcl  12307  uzwo  12314  indstr  12319  zmax  12348  xmulasslem  12681  xrsupsslem  12703  xrinfmsslem  12704  xrsupss  12705  xrinfmss  12706  flval2  13187  om2uzlti  13321  uzrdgfni  13329  rabssnn0fi  13357  mptnn0fsupp  13368  seqcl2  13391  seqfveq2  13395  seqshft2  13399  monoord  13403  seqsplit  13406  seqcaopr3  13408  seqf1olem2a  13411  seqf1o  13414  seqid2  13419  seqhomo  13420  ser1const  13429  expcllem  13443  expeq0  13462  mulexp  13471  expadd  13474  expmul  13477  expmordi  13534  leexp2r  13541  leexp1a  13542  bernneq  13593  modexp  13602  facdiv  13650  faclbnd  13653  faclbnd4lem4  13659  hashgadd  13741  hashxp  13798  hashmap  13799  hashf1lem2  13817  hashf1  13818  seqcoll  13825  wrdind  14086  wrd2ind  14087  pfxccatin12lem3  14096  cshweqrep  14185  2cshwcshw  14189  relexp0g  14383  relexpsucnnr  14386  relexpsucnnl  14393  relexpcnv  14396  relexpnndm  14402  relexpaddnn  14412  dfrtrclrec2  14418  rtrclreclem1  14419  rtrclreclem2  14420  rtrclreclem4  14422  dfrtrcl2  14423  relexpind  14425  reusq0  14824  rlim  14854  rlim2  14855  rlim0  14867  rlim0lt  14868  rlimi  14872  ello12r  14876  ello1mpt  14880  ello1d  14882  elo12r  14887  lo1o1  14891  o1lo1  14896  lo1res  14918  climshft  14935  o1compt  14946  rlimo1  14975  lo1add  14985  lo1mul  14986  rlimdiv  15004  climub  15020  climserle  15021  caucvgrlem  15031  caurcvgr  15032  iseraltlem2  15041  summolem2a  15074  sumss  15083  fsum2d  15128  fsumabs  15158  fsumrlim  15168  fsumo1  15169  fsumiun  15178  binom  15187  climcndslem1  15206  climcndslem2  15207  cvgrat  15241  clim2prod  15246  prodfn0  15252  prodfrec  15253  ntrivcvgfvn0  15257  prodmolem2a  15290  fprodabs  15330  fprodn0  15335  fprod2d  15337  binomfallfac  15397  bpolycl  15408  bpolydif  15411  fprodefsum  15450  demoivreALT  15556  ruclem8  15592  ruclem9  15593  dvdsle  15662  dvdsfac  15678  divalglem7  15752  bitsinv1  15793  sadcadd  15809  sadadd2  15811  saddisjlem  15815  smuval2  15833  smupvallem  15834  smu01lem  15836  smupval  15839  smueqlem  15841  smumullem  15843  bezoutlem4  15892  dfgcd2  15896  gcdmultipleOLD  15902  rplpwr  15909  nn0seqcvgd  15916  seq1st  15917  alginv  15921  algcvga  15925  algfx  15926  lcmf  15979  prmind2  16031  prmdvdsexp  16061  prmfac1  16065  reumodprminv  16143  pcmpt  16230  pcfac  16237  prmpwdvds  16242  prmreclem4  16257  vdwlem10  16328  ramval  16346  ramcl  16367  cshwrepswhash1  16438  prmlem1a  16442  imasleval  16816  ismre  16863  mreexexd  16921  lubprop  17598  lublecllem  17600  glbprop  17611  joinlem  17623  meetlem  17637  isglbd  17729  lubun  17735  poslubmo  17758  posglbmo  17759  poslubd  17760  mndind  17994  frmdgsum  18029  mulgnnass  18264  mhmmulg  18270  gsumwrev  18496  gsmsymgrfix  18558  gsmsymgreq  18562  psgnunilem3  18626  sylow1lem1  18725  efginvrel2  18855  efgsrel  18862  efgredlemd  18872  efgredlem  18875  efgred  18876  efgrelexlemb  18878  gsum2dlem2  19093  gsumcom2  19097  ablfac1eulem  19196  pgpfac1lem2  19199  pgpfac1lem5  19203  pgpfac1  19204  pgpfac  19208  srgmulgass  19283  srgpcomp  19284  srgbinom  19297  lmodvsmmulgdi  19671  isdomn2  20074  assamulgscm  20132  mplcoe1  20248  mplcoe3  20249  mplcoe5  20251  gsummoncoe1  20474  cnfldexp  20580  islindf4  20984  dmatval  21103  dmatel  21104  dmatmulcl  21111  pmatcoe1fsupp  21311  decpmataa0  21378  decpmatmulsumfsupp  21383  pmatcollpw2lem  21387  pm2mpmhmlem1  21428  fiinopn  21511  mretopd  21702  neiptoptop  21741  cnpfval  21844  iscnp3  21854  tgcn  21862  lmbr  21868  lmbr2  21869  lmbrf  21870  lmss  21908  ishaus  21932  hausnei2  21963  t1sep2  21979  fiuncmp  22014  dfconn2  22029  1stcfb  22055  2ndc1stc  22061  1stcrest  22063  1stcelcls  22071  1stccn  22073  lly1stc  22106  elkgen  22146  kgencn  22166  tx1stc  22260  xkopt  22265  cnmptcom  22288  isr0  22347  r0sep  22358  ptcmpfi  22423  isfildlem  22467  rnelfm  22563  fbflim  22586  flimrest  22593  isflf  22603  flffbas  22605  lmflf  22615  fclsrest  22634  isfcf  22644  cnextfvval  22675  tmdgsum  22705  eltsms  22743  tsmsi  22744  tsmsgsum  22749  tsmssubm  22753  tsmsres  22754  tsmsf1o  22755  isust  22814  isucn  22889  isucn2  22890  ucnima  22892  imasdsf1olem  22985  metss  23120  met1stc  23133  metcnp  23153  metcnpi  23156  metcnpi2  23157  metucn  23183  xrge0tsms  23444  fsumcn  23480  elcncf  23499  cncfi  23504  rescncf  23507  cncfco  23517  caucfil  23888  equivcau  23905  caubl  23913  caublcls  23914  ovolgelb  24083  ovolunlem1a  24099  ovolicc2lem3  24122  voliunlem1  24153  voliunlem3  24155  volsuplem  24158  volsup  24159  dyadmax  24201  vitali  24216  itg2leub  24337  itgfsum  24429  dvnadd  24528  dvnres  24530  cpnord  24534  dvnfre  24551  dvmptfsum  24574  dvferm1  24584  dvferm2  24586  rolle  24589  dvlip  24592  c1lip1  24596  lhop1  24613  deg1leb  24691  ply1divex  24732  fta1g  24763  plyco  24833  dgrcolem1  24865  dgrco  24867  dvnply2  24878  plydivex  24888  aalioulem2  24924  aalioulem3  24925  aalioulem5  24927  aaliou3lem2  24934  dvntaylp  24961  taylthlem1  24963  ulmdvlem3  24992  abelthlem9  25030  cxpmul2  25274  scvxcvx  25565  jensenlem2  25567  jensen  25568  wilthlem3  25649  perfectlem2  25808  bcmono  25855  bposlem5  25866  lgsquad2lem2  25963  addsq2reu  26018  2sqreulem1  26024  2sqreunnlem1  26027  dchrisumlem1  26067  dchrisum0flb  26088  pntpbnd1  26164  pntlemf  26183  qabvle  26203  qabvexp  26204  ostthlem2  26206  ostth2lem2  26212  tgcgr4  26319  usgr2pth  27547  wlkiswwlks2lem4  27652  wlkiswwlks2  27655  rusgrnumwwlk  27756  clwlkclwwlklem2a  27778  clwlkclwwlklem1  27779  clwlkclwwlkfo  27789  eupth2  28020  frgr3vlem1  28054  3vfriswmgrlem  28058  3vfriswmgr  28059  wlkl0  28148  numclwlk2lem2f1o  28160  isplig  28255  isnvlem  28389  nvi  28393  nmoubi  28551  nmounbi  28555  nmblolbi  28579  ipasslem1  28610  ipassi  28620  hlim2  28971  pjhth  29172  spansni  29336  elspansn2  29346  pjige0  29470  pjcjt2  29471  pjopyth  29499  elcnop  29636  elcnfn  29661  nmopub  29687  cnopc  29692  nmfnleub  29704  elnlfn  29707  cnfnc  29709  nmbdoplb  29804  nmcexi  29805  nmcoplb  29809  lnfnmul  29827  nmbdfnlb  29829  nmcfnlb  29833  pjss2coi  29943  pjssmi  29944  isst  29992  ishst  29993  stcltr1i  30053  mdbr  30073  dmdbr  30078  mddmd2  30088  mdslmd1lem3  30106  mdslmd1lem4  30107  elat2  30119  atcvat2  30168  cdj1i  30212  iuninc  30314  fmptcof2  30404  nn0min  30538  wrdt2ind  30629  xrge0tsmsd  30694  isomnd  30704  omndadd  30709  cyc3genpm  30796  isarchi2  30816  archirng  30819  archiexdiv  30821  archiabl  30829  isorng  30874  ofldchr  30889  mxidlval  30972  crefeq  31111  nexple  31270  esumfzf  31330  issiga  31373  isrnsiga  31374  isldsys  31417  ismeas  31460  isrnmeas  31461  measiun  31479  eulerpartlemn  31641  sseqp1  31655  rrvsum  31714  signsply0  31823  signstfvc  31846  bnj941  32046  bnj106  32142  bnj155  32153  bnj590  32184  bnj591  32185  bnj849  32199  bnj893  32202  bnj944  32212  bnj1128  32264  subfacp1lem6  32434  erdszelem8  32447  issconn  32475  cvmliftlem7  32540  cvmliftlem10  32543  cvmlift3lem2  32569  satfsschain  32613  satfrel  32616  satfdm  32618  satfrnmapom  32619  fmlafvel  32634  satffun  32658  mrsubvrs  32771  mclsssvlem  32811  mclsval  32812  mclsax  32818  mclsind  32819  shftvalg  32965  bccolsum  32973  iprodefisumlem  32974  faclimlem1  32977  dfpo2  32993  rdgprc  33041  trpredmintr  33072  frmin  33086  soseq  33098  frr3g  33123  fpr3g  33124  frrlem12  33136  fpr2  33142  frr2  33147  nosupno  33205  nosupdm  33206  nosupfv  33208  nosupres  33209  nosupbnd1lem1  33210  nosupbnd1lem3  33212  nosupbnd1lem5  33214  noeta  33224  fveleq  33801  unblimceq0  33848  bj-ax12  33992  bj-bm1.3ii  34359  rdgeqoa  34653  finxpreclem6  34679  domalom  34687  ralssiun  34690  wl-sblimt  34789  wl-sbhbt  34792  wl-2sb6d  34796  wl-mo2df  34808  wl-mo2t  34813  poimirlem2  34896  poimirlem25  34919  poimirlem28  34922  poimirlem31  34925  heicant  34929  mbfresfi  34940  itg2gt0cn  34949  sdclem2  35019  fdc  35022  seqpo  35024  incsequz  35025  mettrifi  35034  prdsbnd2  35075  heiborlem4  35094  bfplem1  35102  iscringd  35278  maxidlval  35319  igenval2  35346  iss2  35603  elrefrels3  35760  ax12eq  36079  ax12el  36080  ax12indalem  36083  ax12inda2ALT  36084  ax12inda  36086  ax12v2-o  36087  riotasvd  36094  isopos  36318  isat3  36445  ishlat1  36490  glbconN  36515  ispsubsp  36883  isldil  37248  isltrn  37257  isdilN  37292  trlval  37300  cdleme27b  37506  cdleme29b  37513  cdleme31sn1  37519  cdleme31sn1c  37526  cdleme40v  37607  cdlemk36  38051  cdlemkid5  38073  cdlemn11pre  38348  dihord2pre  38363  islpolN  38621  hdmapffval  38964  hdmapfval  38965  hdmapval2lem  38969  nnaddcom  39168  nnadddir  39170  nnmulcom  39172  ismrc  39305  incssnn0  39315  mzpexpmpt  39349  pell14qrexpclnn0  39470  monotuz  39545  rmxypos  39551  jm2.17a  39564  jm2.17b  39565  rmygeid  39568  jm2.18  39592  jm2.19lem3  39595  jm2.25  39603  jm2.15nn0  39607  jm2.16nn0  39608  wepwsolem  39649  aomclem8  39668  dfac11  39669  pwslnm  39701  lnr2i  39723  hbtlem5  39735  cnsrexpcl  39772  rngunsnply  39780  isdomn3  39811  ifpbi23  39845  elmapintrab  39943  elmapintab  39963  cnvcnvintabd  39967  eliunov2  40031  relexpxpnnidm  40055  relexpiidm  40056  relexpss1d  40057  iunrelexpmin1  40060  relexpmulnn  40061  iunrelexpmin2  40064  relexp0a  40068  trclimalb2  40078  clsk3nimkb  40397  ntrclsiso  40424  ntrclskb  40426  ntrneiiso  40448  ntrneix2  40450  ntrneixb  40452  gneispace2  40489  gneispacess2  40503  mnuunid  40620  dvgrat  40651  pm14.122b  40762  fnchoice  41293  fiiuncl  41334  ssinc  41360  ssdec  41361  wessf1ornlem  41452  dmrelrnrel  41497  fperiodmullem  41577  monoordxrv  41765  fmul01  41868  fmuldfeq  41871  climsuselem1  41895  climinff  41899  ellimcabssub0  41905  limcleqr  41932  addlimc  41936  0ellimcdiv  41937  limclner  41939  limsupref  41973  limsupub  41992  limsupmnf  42009  limsupre2lem  42012  limsupre2  42013  limsupre2mpt  42018  limsupre3lem  42020  limsupre3  42021  limsupre3mpt  42022  xlimbr  42115  cnrefiisplem  42117  dvnmptdivc  42230  dvnmptconst  42233  dvnmul  42235  iblspltprt  42265  itgspltprt  42271  stoweidlem2  42294  stoweidlem3  42295  stoweidlem17  42309  stoweidlem19  42311  stoweidlem21  42313  stoweidlem26  42318  fourierdlem42  42441  issal  42606  ismea  42740  isome  42783  carageniuncllem1  42810  caratheodorylem1  42815  2reu8i  43319  2reuimp0  43320  funressndmafv2rn  43429  2ffzoeq  43535  smonoord  43538  fargshiftf1  43608  paireqne  43680  reupr  43691  reuopreuprim  43695  perfectALTVlem2  43894  lmodvsmdi  44437  dmatALTval  44462  dmatALTbasel  44464  snlindsntor  44533  ldepsnlinc  44570  elbigo2r  44620  elbigolo1  44624  setrecseq  44795  setrec2fun  44802  setrec2lem2  44804