Theorem imbi2d 317

Description: Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.)

Hypothesis

Ref	Expression
imbid.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
imbi2d	|- ( ph -> ( ( th -> ps ) <-> ( th -> ch ) ) )

Proof of Theorem imbi2d

Step	Hyp	Ref	Expression
1		imbid.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	a1d 26	. 2 |- ( ph -> ( th -> ( ps <-> ch ) ) )
3	2	pm5.74d 250	1 |- ( ph -> ( ( th -> ps ) <-> ( th -> ch ) ) )

Syntax hints:   -> wi 4   <-> wb 187

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 188

This theorem is referenced by:  imbi12d  321  imbi2  325  pm5.42  550  orbi2d  706  con3th  966  ax12vOLD  1906  ax12v2  2136  axc14  2164  mo2  2273  2gencl  3109  3gencl  3110  vtocl2gf  3138  vtocl3gf  3139  vtocl4g  3147  eqeu  3239  mo2icl  3247  euind  3255  reu7  3263  reuind  3272  sbctt  3359  sbcnestgf  3809  r19.36zv  3895  dedth2h  3958  dedth3h  3959  dedth4h  3960  preq12bg  4173  prel12g  4174  elint  4255  elintrabg  4262  intab  4280  trss  4520  axrep1  4530  axrep2  4531  axrep3  4532  bm1.3ii  4542  reusv3  4624  pocl  4773  swopolem  4775  solin  4789  freq1  4815  frminex  4825  vtoclr  4890  2optocl  4923  3optocl  4924  raliunxp  4985  resieq  5126  iss  5163  cnveqb  5302  preddowncl  5417  funmo  5608  funimaexg  5669  fnbrfvb  5912  fvelimab  5928  fvmptss  5965  fmptco  6062  fprg  6079  fnressn  6082  fressnfv  6084  isoselem  6238  ovg  6440  caovcan  6478  caovordig  6479  caovord  6485  tfisi  6690  tfindsg  6692  tfinds2  6695  tfinds3  6696  dfom2  6699  elom  6700  findsg  6725  finds2  6726  f1o2ndf1  6906  poxp  6910  fnse  6915  wfr3g  7033  wfrlem4  7038  smoeq  7068  smores  7070  smogt  7085  tfrlem1  7093  tfr3  7116  oaordi  7246  oeordi  7287  oeoa  7297  oeoe  7299  nnacl  7311  nnmcl  7312  nnecl  7313  nnacom  7317  nnaordi  7318  nnawordi  7321  nnaass  7322  nndi  7323  nnmass  7324  nnmsucr  7325  nnmcom  7326  nnmordi  7331  2ecoptocl  7453  3ecoptocl  7454  undifixp  7557  xpdom2g  7665  findcard2  7808  xpfi  7839  fnfi  7846  fodomfi  7847  finsschain  7878  marypha1lem  7944  marypha1  7945  supeq1  7956  ordiso2  8021  ordtypelem7  8030  wemaplem1  8052  inf3lem2  8125  inf3lem5  8128  infdiffi  8153  cantnfval2  8164  cantnfle  8166  cantnfp1lem3  8175  oemapval  8178  cantnflem1  8184  cantnf  8188  wemapwe  8192  cnfcom  8195  cnfcom3clem  8200  tz9.1  8203  r1pwALT  8307  cplem2  8351  karden  8356  infxpenc2lem2  8440  fseqenlem1  8444  dfac8clem  8452  alephinit  8515  dfac4  8542  dfac5lem5  8547  dfac2a  8549  dfac2  8550  dfacacn  8560  dfac12lem3  8564  kmlem2  8570  kmlem13  8581  ackbij1lem16  8654  sornom  8696  infpssrlem4  8725  fin23lem14  8752  fin23lem32  8763  fin23lem34  8765  fin23lem36  8767  isf32lem1  8772  isf32lem2  8773  axcc2lem  8855  axcc3  8857  axcclem  8876  zornn0g  8924  ttukeylem5  8932  ttukeylem6  8933  axrepnd  9008  axpowndlem3  9013  zfcndrep  9028  fpwwe2lem8  9051  pwfseqlem3  9074  wunr1om  9133  wunfi  9135  tskr1om  9181  ingru  9229  grudomon  9231  axgroth3  9245  axgroth4  9246  nqereu  9343  mulcanenq  9374  elnp  9401  elnpi  9402  prlem934  9447  infm3  10557  nnaddcl  10620  nnmulcl  10621  peano5uzi  11013  uzind2  11017  nn0indd  11021  zindd  11025  eluzadd  11176  uzaddcl  11204  uzwo  11211  indstr  11216  zmax  11250  xmulasslem  11560  xrsupsslem  11581  xrinfmsslem  11582  xrsupss  11583  xrinfmss  11584  flval2  12035  om2uzlti  12150  uzrdgfni  12158  rabssnn0fi  12184  mptnn0fsupp  12195  seqcl2  12217  seqfveq2  12221  seqshft2  12225  monoord  12229  seqsplit  12232  seqcaopr3  12234  seqf1olem2a  12237  seqf1o  12240  seqid2  12245  seqhomo  12246  ser1const  12255  expcllem  12269  expeq0  12288  mulexp  12297  expadd  12300  expmul  12303  leexp2r  12316  leexp1a  12317  bernneq  12384  modexp  12393  facdiv  12458  faclbnd  12461  faclbnd4lem4  12467  faclbnd6  12470  hashgadd  12542  hashxp  12590  hashmap  12591  hashf1lem2  12603  hashf1  12604  seqcoll  12610  wrdind  12807  wrd2ind  12808  swrdccatin12lem3  12820  cshweqrep  12894  2cshwcshw  12898  relexp0g  13053  relexpsucnnr  13056  relexpsucnnl  13063  relexpcnv  13066  relexpnndm  13072  relexpaddnn  13082  dfrtrclrec2  13088  rtrclreclem1  13089  rtrclreclem2  13090  rtrclreclem4  13092  dfrtrcl2  13093  relexpind  13095  cjexp  13181  absexp  13335  rlim  13526  rlim2  13527  rlim0  13539  rlim0lt  13540  rlimi  13544  ello12r  13548  ello1mpt  13552  ello1d  13554  elo12r  13559  lo1o1  13563  o1lo1  13568  lo1res  13590  climshft  13607  o1compt  13618  rlimo1  13647  lo1add  13657  lo1mul  13658  rlimdiv  13676  climub  13692  climserle  13693  caucvgrlem  13703  caucvgrlemOLD  13704  caurcvgr  13705  caurcvgrOLD  13706  iseraltlem2  13716  summolem2a  13748  sumss  13757  fsum2d  13799  fsumabs  13828  fsumrlim  13838  fsumo1  13839  fsumiun  13848  binom  13855  bcxmas  13860  climcndslem1  13874  climcndslem2  13875  cvgrat  13906  clim2prod  13911  prodfn0  13917  prodfrec  13918  ntrivcvgfvn0  13922  prodmolem2a  13955  fprodabs  13995  fprodn0  14000  fprod2d  14002  binomfallfac  14061  bpolycl  14072  bpolydif  14075  fprodefsum  14116  demoivreALT  14222  ruclem8  14256  ruclem9  14257  dvdsle  14317  dvdsfac  14327  divalglem7  14344  bitsinv1  14379  sadcadd  14395  sadadd2  14397  saddisjlem  14401  smuval2  14419  smupvallem  14420  smu01lem  14422  smupval  14425  smueqlem  14427  smumullem  14429  bezoutlem4  14469  gcdmultiple  14478  rplpwr  14484  nn0seqcvgd  14489  seq1st  14490  alginv  14494  algcvga  14498  algfx  14499  lcmf  14566  prmind2  14595  prmdvdsexp  14627  prmfac1  14631  reumodprminv  14707  pcmpt  14789  pcfac  14796  prmpwdvds  14800  prmreclem4  14815  vdwlem10  14892  ramval  14912  ramvalOLD  14913  ramcl  14939  cshwrepswhash1  15025  prmlem1a  15030  imasleval  15391  ismre  15440  mreexexd  15498  lubprop  16176  lublecllem  16178  glbprop  16189  joinlem  16201  meetlem  16215  isglbd  16307  lubun  16313  poslubmo  16336  posglbmo  16337  poslubd  16338  mrcmndind  16557  frmdgsum  16590  mulgnnass  16730  mhmmulg  16734  gsumwrev  16961  gsmsymgrfix  17013  gsmsymgreq  17017  psgnunilem3  17081  sylow1lem1  17178  efginvrel2  17305  efgsrel  17312  efgredlemd  17322  efgredlem  17325  efgred  17326  efgrelexlemb  17328  gsum2dlem2  17531  gsumcom2  17535  ablfac1eulem  17633  pgpfac1lem2  17636  pgpfac1lem5  17640  pgpfac1  17641  pgpfac  17645  srgmulgass  17692  srgpcomp  17693  srgbinom  17706  lmodvsmmulgdi  18054  isdomn2  18451  assamulgscm  18502  mplcoe1  18617  mplcoe3  18618  mplcoe5  18620  gsummoncoe1  18826  cnfldexp  18929  islindf4  19320  dmatval  19441  dmatel  19442  dmatmulcl  19449  pmatcoe1fsupp  19649  decpmataa0  19716  decpmatmulsumfsupp  19721  pmatcollpw2lem  19725  pm2mpmhmlem1  19766  fiinopn  19855  mretopd  20032  neiptoptop  20071  cnpfval  20174  iscnp3  20184  tgcn  20192  lmbr  20198  lmbr2  20199  lmbrf  20200  lmss  20238  ishaus  20262  hausnei2  20293  t1sep2  20309  fiuncmp  20343  dfcon2  20358  1stcfb  20384  2ndc1stc  20390  1stcrest  20392  1stcelcls  20400  1stccn  20402  lly1stc  20435  elkgen  20475  kgencn  20495  tx1stc  20589  xkopt  20594  cnmptcom  20617  isr0  20676  r0sep  20687  ptcmpfi  20752  isfildlem  20796  rnelfm  20892  fbflim  20915  flimrest  20922  isflf  20932  flffbas  20934  lmflf  20944  fclsrest  20963  isfcf  20973  cnextfvval  21004  tmdmulg  21031  tmdgsum  21034  eltsms  21071  tsmsi  21072  tsmsgsum  21077  tsmssubm  21081  tsmsres  21082  tsmsf1o  21083  isust  21142  isucn  21217  isucn2  21218  ucnima  21220  imasdsf1olem  21312  metss  21447  met1stc  21460  metcnp  21480  metcnpi  21483  metcnpi2  21484  metucn  21510  xrge0tsms  21756  fsumcn  21791  elcncf  21810  cncfi  21815  rescncf  21818  cncfco  21828  caucfil  22139  equivcau  22156  caubl  22163  caublcls  22164  ovolgelb  22307  ovolunlem1a  22323  ovolicc2lem3  22346  voliunlem1  22377  voliunlem3  22379  volsuplem  22382  volsup  22383  dyadmax  22430  vitali  22445  itg2leub  22566  itgfsum  22658  dvnadd  22757  dvnres  22759  cpnord  22763  dvnfre  22780  dvmptfsum  22801  dvferm1  22811  dvferm2  22813  rolle  22816  dvlip  22819  c1lip1  22823  lhop1  22840  deg1leb  22918  ply1divex  22959  fta1g  22990  plyco  23060  dgrcolem1  23092  dgrco  23094  dvnply2  23105  plydivex  23115  aalioulem2  23151  aalioulem3  23152  aalioulem5  23154  aaliou3lem2  23161  dvntaylp  23188  taylthlem1  23190  ulmdvlem3  23219  abelthlem9  23257  cxpmul2  23496  scvxcvx  23773  jensenlem2  23775  jensen  23776  wilthlem3  23857  perfectlem2  24018  bcmono  24065  bposlem5  24076  lgsquad2lem2  24147  dchrisumlem1  24187  dchrisum0flb  24208  pntpbnd1  24284  pntlemf  24303  qabvle  24323  qabvexp  24324  ostthlem2  24326  ostth2lem2  24332  sizeusglecusglem1  25054  2pthoncl  25175  fargshiftf1  25207  3v3e3cycl1  25214  4cycl4v4e  25236  4cycl4dv4e  25238  wlkiswwlk2lem4  25264  wlkiswwlk2  25267  clwlkisclwwlklem2a  25355  clwlkisclwwlklem2  25356  clwlkfoclwwlk  25415  el2wlkonot  25439  el2spthonot  25440  rusgranumwlk  25527  eupatrl  25538  eupath2  25550  frgra3vlem1  25570  3vfriswmgralem  25574  usg2spot2nb  25635  2spotmdisj  25638  numclwlk2lem2f1o  25675  isplig  25751  gxnn0add  25844  gxnn0mul  25847  ghgrpOLD  25938  ghabloOLD  25939  isnvlem  26071  nvi  26075  nmoubi  26255  nmounbi  26259  nmblolbi  26283  ipasslem1  26314  ipassi  26324  hlim2  26677  pjhth  26878  spansni  27042  elspansn2  27052  pjige0  27176  pjcjt2  27177  pjopyth  27205  elcnop  27342  elcnfn  27367  nmopub  27393  cnopc  27398  nmfnleub  27410  elnlfn  27413  cnfnc  27415  nmbdoplb  27510  nmcexi  27511  nmcoplb  27515  lnfnmul  27533  nmbdfnlb  27535  nmcfnlb  27539  pjss2coi  27649  pjssmi  27650  isst  27698  ishst  27699  stcltr1i  27759  mdbr  27779  dmdbr  27784  mddmd2  27794  mdslmd1lem3  27812  mdslmd1lem4  27813  elat2  27825  atcvat2  27874  cdj1i  27918  vtocl2d  27941  rmoeq  27955  iuninc  28012  fmptcof2  28096  nnindd  28218  nn0min  28219  isomnd  28299  omndadd  28304  isarchi2  28337  archirng  28340  archiexdiv  28342  archiabl  28350  xrge0tsmsd  28384  isorng  28398  ofldchr  28413  crefeq  28508  nexple  28667  esumfzf  28726  issiga  28769  isrnsiga  28771  isldsys  28814  ismeas  28857  isrnmeas  28858  measiun  28876  eulerpartlemn  29037  sseqp1  29051  rrvsum  29110  signsply0  29225  signstfvc  29248  bnj941  29369  bnj106  29464  bnj155  29475  bnj590  29506  bnj591  29507  bnj849  29521  bnj893  29524  bnj944  29534  bnj1128  29584  subfacp1lem6  29693  erdszelem8  29706  isscon  29734  cvmliftlem7  29799  cvmliftlem10  29802  cvmlift3lem2  29828  mrsubvrs  29945  mclsssvlem  29985  mclsval  29986  mclsax  29992  mclsind  29993  ghomf1olem  30097  shftvalg  30149  bccolsum  30159  iprodefisumlem  30160  faclimlem1  30163  dfpo2  30179  br1steqg  30200  br2ndeqg  30201  rdgprc  30225  trpredmintr  30256  frmin  30264  soseq  30276  frr3g  30297  fveleq  30893  bj-con3thALT  30937  bj-axc15v  31107  bj-axrep1  31151  bj-axrep2  31152  bj-axrep3  31153  wl-sblimt  31583  wl-sbhbt  31586  wl-2sb6d  31592  wl-mo2df  31603  wl-mo2t  31608  wl-ax12v3  31616  poimirlem2  31646  poimirlem25  31669  poimirlem28  31672  poimirlem31  31675  heicant  31679  mbfresfi  31691  itg2gt0cn  31701  sdclem2  31775  fdc  31778  seqpo  31780  incsequz  31781  mettrifi  31790  prdsbnd2  31831  heiborlem4  31850  bfplem1  31858  iscringd  31936  maxidlval  31976  igenval2  32003  ax12eq  32221  ax12el  32222  ax12indalem  32225  ax12inda2ALT  32226  ax12inda  32228  ax12v2-o  32229  riotasvd  32237  isopos  32455  isat3  32582  ishlat1  32627  glbconN  32651  ispsubsp  33019  isldil  33384  isltrn  33393  isdilN  33429  trlval  33437  cdleme27b  33644  cdleme29b  33651  cdleme31sn1  33657  cdleme31sn1c  33664  cdleme40v  33745  cdlemk36  34189  cdlemkid5  34211  cdlemn11pre  34487  dihord2pre  34502  islpolN  34760  hdmapffval  35106  hdmapfval  35107  hdmapval2lem  35111  ismrc  35252  incssnn0  35262  mzpexpmpt  35296  pell14qrexpclnn0  35422  monotuz  35499  expmordi  35505  rmxypos  35507  jm2.17a  35520  jm2.17b  35521  rmygeid  35524  divalgmodcl  35552  jm2.18  35553  jm2.19lem3  35556  jm2.25  35564  jm2.15nn0  35568  jm2.16nn0  35569  wepwsolem  35610  aomclem8  35629  dfac11  35630  pwslnm  35662  lnr2i  35685  hbtlem5  35697  cnsrexpcl  35734  rngunsnply  35742  isdomn3  35784  ifpbi23  35819  eliunov2  35914  relexpxpnnidm  35938  relexpiidm  35939  relexpss1d  35940  iunrelexpmin1  35943  relexpmulnn  35944  iunrelexpmin2  35947  relexp0a  35951  trclimalb2  35961  dvgrat  36302  pm14.122b  36415  fnchoice  36994  fiiuncl  37052  wessf1ornlem  37086  fperiodmullem  37134  fmul01  37234  fmuldfeq  37237  climsuselem1  37262  climinff  37266  climinffOLD  37267  ellimcabssub0  37273  limcleqr  37301  addlimc  37305  0ellimcdiv  37306  limclner  37308  dvnmptdivc  37386  dvnmptconst  37389  dvnmul  37391  iblspltprt  37423  itgspltprt  37429  stoweidlem2  37435  stoweidlem3  37436  stoweidlem17  37450  stoweidlem19  37452  stoweidlem21  37454  stoweidlem26  37459  fourierdlem42  37584  issal  37726  ismea  37802  isome  37828  carageniuncllem1  37855  caratheodorylem1  37860  smonoord  38121  perfectALTVlem2  38247  2ffzoeq  38426  usgra2pth  38437  usgfis  38529  lmodvsmdi  38940  dmatALTval  38966  dmatALTbasel  38968  snlindsntor  39037  ldepsnlinc  39074  elbigo2r  39138  elbigolo1  39142