Theorem imbi2d 322

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 255	1 |- ( ph -> ( ( th -> ps ) <-> ( th -> ch ) ) )

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

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 190

This theorem is referenced by:  imbi12d  326  imbi2  330  pm5.42  555  orbi2d  713  con3th  975  ax12v2  2186  axc14  2212  mo2  2319  2gencl  3090  3gencl  3091  vtocl2gf  3121  vtocl3gf  3122  vtocl4g  3130  eqeu  3221  mo2icl  3229  euind  3237  reu7  3245  reuind  3255  sbctt  3342  sbcnestgf  3796  r19.36zv  3882  dedth2h  3945  dedth3h  3946  dedth4h  3947  preq12bg  4168  prel12g  4169  elint  4254  elintrabg  4261  intab  4279  trss  4522  axrep1  4532  axrep2  4533  axrep3  4534  bm1.3ii  4544  reusv3  4628  pocl  4784  swopolem  4786  solin  4800  freq1  4826  frminex  4836  vtoclr  4901  2optocl  4934  3optocl  4935  raliunxp  4996  resieq  5137  iss  5174  cnveqb  5314  preddowncl  5430  funmo  5621  funimaexg  5686  fnbrfvb  5932  fvelimab  5949  fvmptss  5986  fmptco  6085  fprg  6102  fnressn  6105  fressnfv  6107  isoselem  6262  ovg  6467  caovcan  6505  caovordig  6506  caovord  6512  tfisi  6717  tfindsg  6719  tfinds2  6722  tfinds3  6723  dfom2  6726  elom  6727  findsg  6752  finds2  6753  f1o2ndf1  6936  poxp  6940  fnse  6945  wfr3g  7065  wfrlem4  7070  smoeq  7100  smores  7102  smogt  7117  tfrlem1  7125  tfr3  7148  oaordi  7278  oeordi  7319  oeoa  7329  oeoe  7331  nnacl  7343  nnmcl  7344  nnecl  7345  nnacom  7349  nnaordi  7350  nnawordi  7353  nnaass  7354  nndi  7355  nnmass  7356  nnmsucr  7357  nnmcom  7358  nnmordi  7363  2ecoptocl  7485  3ecoptocl  7486  undifixp  7589  xpdom2g  7699  findcard2  7842  xpfi  7873  fnfi  7880  fodomfi  7881  finsschain  7912  marypha1lem  7978  marypha1  7979  supeq1  7990  ordiso2  8061  ordtypelem7  8070  wemaplem1  8092  inf3lem2  8165  inf3lem5  8168  infdiffi  8194  cantnfval2  8205  cantnfle  8207  cantnfp1lem3  8216  oemapval  8219  cantnflem1  8225  cantnf  8229  wemapwe  8233  cnfcom  8236  cnfcom3clem  8241  tz9.1  8244  r1pwALT  8348  cplem2  8392  karden  8397  infxpenc2lem2  8482  fseqenlem1  8486  dfac8clem  8494  alephinit  8557  dfac4  8584  dfac5lem5  8589  dfac2a  8591  dfac2  8592  dfacacn  8602  dfac12lem3  8606  kmlem2  8612  kmlem13  8623  ackbij1lem16  8696  sornom  8738  infpssrlem4  8767  fin23lem14  8794  fin23lem32  8805  fin23lem34  8807  fin23lem36  8809  isf32lem1  8814  isf32lem2  8815  axcc2lem  8897  axcc3  8899  axcclem  8918  zornn0g  8966  ttukeylem5  8974  ttukeylem6  8975  axrepnd  9050  axpowndlem3  9055  zfcndrep  9070  fpwwe2lem8  9093  pwfseqlem3  9116  wunr1om  9175  wunfi  9177  tskr1om  9223  ingru  9271  grudomon  9273  axgroth3  9287  axgroth4  9288  nqereu  9385  mulcanenq  9416  elnp  9443  elnpi  9444  prlem934  9489  infm3  10601  nnaddcl  10664  nnmulcl  10665  peano5uzi  11058  uzind2  11062  nn0indd  11066  zindd  11070  eluzadd  11221  uzaddcl  11249  uzwo  11256  indstr  11261  zmax  11295  xmulasslem  11605  xrsupsslem  11626  xrinfmsslem  11627  xrsupss  11628  xrinfmss  11629  flval2  12087  om2uzlti  12202  uzrdgfni  12210  rabssnn0fi  12236  mptnn0fsupp  12247  seqcl2  12269  seqfveq2  12273  seqshft2  12277  monoord  12281  seqsplit  12284  seqcaopr3  12286  seqf1olem2a  12289  seqf1o  12292  seqid2  12297  seqhomo  12298  ser1const  12307  expcllem  12321  expeq0  12340  mulexp  12349  expadd  12352  expmul  12355  leexp2r  12368  leexp1a  12369  bernneq  12436  modexp  12445  facdiv  12510  faclbnd  12513  faclbnd4lem4  12519  faclbnd6  12522  hashgadd  12594  hashxp  12645  hashmap  12646  hashf1lem2  12658  hashf1  12659  seqcoll  12666  wrdind  12876  wrd2ind  12877  swrdccatin12lem3  12889  cshweqrep  12963  2cshwcshw  12967  relexp0g  13140  relexpsucnnr  13143  relexpsucnnl  13150  relexpcnv  13153  relexpnndm  13159  relexpaddnn  13169  dfrtrclrec2  13175  rtrclreclem1  13176  rtrclreclem2  13177  rtrclreclem4  13179  dfrtrcl2  13180  relexpind  13182  cjexp  13268  absexp  13422  rlim  13614  rlim2  13615  rlim0  13627  rlim0lt  13628  rlimi  13632  ello12r  13636  ello1mpt  13640  ello1d  13642  elo12r  13647  lo1o1  13651  o1lo1  13656  lo1res  13678  climshft  13695  o1compt  13706  rlimo1  13735  lo1add  13745  lo1mul  13746  rlimdiv  13764  climub  13780  climserle  13781  caucvgrlem  13791  caucvgrlemOLD  13792  caurcvgr  13793  caurcvgrOLD  13794  iseraltlem2  13804  summolem2a  13836  sumss  13845  fsum2d  13887  fsumabs  13916  fsumrlim  13926  fsumo1  13927  fsumiun  13936  binom  13943  bcxmas  13948  climcndslem1  13962  climcndslem2  13963  cvgrat  13994  clim2prod  13999  prodfn0  14005  prodfrec  14006  ntrivcvgfvn0  14010  prodmolem2a  14043  fprodabs  14083  fprodn0  14088  fprod2d  14090  binomfallfac  14149  bpolycl  14160  bpolydif  14163  fprodefsum  14204  demoivreALT  14310  ruclem8  14344  ruclem9  14345  dvdsle  14405  dvdsfac  14415  divalglem7  14434  bitsinv1  14471  sadcadd  14487  sadadd2  14489  saddisjlem  14493  smuval2  14511  smupvallem  14512  smu01lem  14514  smupval  14517  smueqlem  14519  smumullem  14521  bezoutlem4OLD  14561  bezoutlem4  14564  gcdmultiple  14573  rplpwr  14579  nn0seqcvgd  14584  seq1st  14585  alginv  14589  algcvga  14593  algfx  14594  lcmf  14661  prmind2  14690  prmdvdsexp  14722  prmfac1  14726  reumodprminv  14810  pcmpt  14892  pcfac  14899  prmpwdvds  14903  prmreclem4  14918  vdwlem10  14995  ramval  15015  ramvalOLD  15016  ramcl  15042  cshwrepswhash1  15128  prmlem1a  15133  imasleval  15502  ismre  15551  mreexexd  15609  lubprop  16287  lublecllem  16289  glbprop  16300  joinlem  16312  meetlem  16326  isglbd  16418  lubun  16424  poslubmo  16447  posglbmo  16448  poslubd  16449  mrcmndind  16668  frmdgsum  16701  mulgnnass  16841  mhmmulg  16845  gsumwrev  17072  gsmsymgrfix  17124  gsmsymgreq  17128  psgnunilem3  17192  sylow1lem1  17305  efginvrel2  17432  efgsrel  17439  efgredlemd  17449  efgredlem  17452  efgred  17453  efgrelexlemb  17455  gsum2dlem2  17658  gsumcom2  17662  ablfac1eulem  17760  pgpfac1lem2  17763  pgpfac1lem5  17767  pgpfac1  17768  pgpfac  17772  srgmulgass  17819  srgpcomp  17820  srgbinom  17833  lmodvsmmulgdi  18181  isdomn2  18578  assamulgscm  18629  mplcoe1  18744  mplcoe3  18745  mplcoe5  18747  gsummoncoe1  18953  cnfldexp  19056  islindf4  19451  dmatval  19572  dmatel  19573  dmatmulcl  19580  pmatcoe1fsupp  19780  decpmataa0  19847  decpmatmulsumfsupp  19852  pmatcollpw2lem  19856  pm2mpmhmlem1  19897  fiinopn  19986  mretopd  20163  neiptoptop  20202  cnpfval  20305  iscnp3  20315  tgcn  20323  lmbr  20329  lmbr2  20330  lmbrf  20331  lmss  20369  ishaus  20393  hausnei2  20424  t1sep2  20440  fiuncmp  20474  dfcon2  20489  1stcfb  20515  2ndc1stc  20521  1stcrest  20523  1stcelcls  20531  1stccn  20533  lly1stc  20566  elkgen  20606  kgencn  20626  tx1stc  20720  xkopt  20725  cnmptcom  20748  isr0  20807  r0sep  20818  ptcmpfi  20883  isfildlem  20927  rnelfm  21023  fbflim  21046  flimrest  21053  isflf  21063  flffbas  21065  lmflf  21075  fclsrest  21094  isfcf  21104  cnextfvval  21135  tmdmulg  21162  tmdgsum  21165  eltsms  21202  tsmsi  21203  tsmsgsum  21208  tsmssubm  21212  tsmsres  21213  tsmsf1o  21214  isust  21273  isucn  21348  isucn2  21349  ucnima  21351  imasdsf1olem  21443  metss  21578  met1stc  21591  metcnp  21611  metcnpi  21614  metcnpi2  21615  metucn  21641  xrge0tsms  21907  fsumcn  21957  elcncf  21976  cncfi  21981  rescncf  21984  cncfco  21994  caucfil  22308  equivcau  22325  caubl  22332  caublcls  22333  ovolgelb  22488  ovolunlem1a  22504  ovolicc2lem3  22527  voliunlem1  22559  voliunlem3  22561  volsuplem  22564  volsup  22565  dyadmax  22612  vitali  22627  itg2leub  22748  itgfsum  22840  dvnadd  22939  dvnres  22941  cpnord  22945  dvnfre  22962  dvmptfsum  22983  dvferm1  22993  dvferm2  22995  rolle  22998  dvlip  23001  c1lip1  23005  lhop1  23022  deg1leb  23100  ply1divex  23143  fta1g  23174  plyco  23251  dgrcolem1  23283  dgrco  23285  dvnply2  23296  plydivex  23306  aalioulem2  23345  aalioulem3  23346  aalioulem5  23348  aaliou3lem2  23355  dvntaylp  23382  taylthlem1  23384  ulmdvlem3  23413  abelthlem9  23451  cxpmul2  23690  scvxcvx  23967  jensenlem2  23969  jensen  23970  wilthlem3  24051  perfectlem2  24214  bcmono  24261  bposlem5  24272  lgsquad2lem2  24343  dchrisumlem1  24383  dchrisum0flb  24404  pntpbnd1  24480  pntlemf  24499  qabvle  24519  qabvexp  24520  ostthlem2  24522  ostth2lem2  24528  tgcgr4  24632  sizeusglecusglem1  25268  2pthoncl  25389  fargshiftf1  25421  3v3e3cycl1  25428  4cycl4v4e  25450  4cycl4dv4e  25452  wlkiswwlk2lem4  25478  wlkiswwlk2  25481  clwlkisclwwlklem2a  25569  clwlkisclwwlklem2  25570  clwlkfoclwwlk  25629  el2wlkonot  25653  el2spthonot  25654  rusgranumwlk  25741  eupatrl  25752  eupath2  25764  frgra3vlem1  25784  3vfriswmgralem  25788  usg2spot2nb  25849  2spotmdisj  25852  numclwlk2lem2f1o  25889  isplig  25965  gxnn0add  26058  gxnn0mul  26061  ghgrpOLD  26152  ghabloOLD  26153  isnvlem  26285  nvi  26289  nmoubi  26469  nmounbi  26473  nmblolbi  26497  ipasslem1  26528  ipassi  26538  hlim2  26901  pjhth  27102  spansni  27266  elspansn2  27276  pjige0  27400  pjcjt2  27401  pjopyth  27429  elcnop  27566  elcnfn  27591  nmopub  27617  cnopc  27622  nmfnleub  27634  elnlfn  27637  cnfnc  27639  nmbdoplb  27734  nmcexi  27735  nmcoplb  27739  lnfnmul  27757  nmbdfnlb  27759  nmcfnlb  27763  pjss2coi  27873  pjssmi  27874  isst  27922  ishst  27923  stcltr1i  27983  mdbr  28003  dmdbr  28008  mddmd2  28018  mdslmd1lem3  28036  mdslmd1lem4  28037  elat2  28049  atcvat2  28098  cdj1i  28142  vtocl2d  28165  rmoeqALT  28179  iuninc  28230  fmptcof2  28311  nnindd  28435  nn0min  28436  isomnd  28515  omndadd  28520  isarchi2  28553  archirng  28556  archiexdiv  28558  archiabl  28566  xrge0tsmsd  28599  isorng  28613  ofldchr  28628  crefeq  28723  nexple  28882  esumfzf  28941  issiga  28984  isrnsiga  28986  isldsys  29029  ismeas  29072  isrnmeas  29073  measiun  29091  eulerpartlemn  29264  sseqp1  29278  rrvsum  29337  signsply0  29490  signstfvc  29513  bnj941  29634  bnj106  29729  bnj155  29740  bnj590  29771  bnj591  29772  bnj849  29786  bnj893  29789  bnj944  29799  bnj1128  29849  subfacp1lem6  29958  erdszelem8  29971  isscon  29999  cvmliftlem7  30064  cvmliftlem10  30067  cvmlift3lem2  30093  mrsubvrs  30210  mclsssvlem  30250  mclsval  30251  mclsax  30257  mclsind  30258  ghomf1olem  30362  shftvalg  30415  bccolsum  30425  iprodefisumlem  30426  faclimlem1  30429  dfpo2  30445  br1steqg  30466  br2ndeqg  30467  rdgprc  30491  trpredmintr  30522  frmin  30530  soseq  30542  frr3g  30563  fveleq  31161  bj-con3thALT  31201  bj-axc15v  31408  bj-axrep1  31449  bj-axrep2  31450  bj-axrep3  31451  rdgeqoa  31819  finxpreclem6  31834  wl-sblimt  31925  wl-sbhbt  31928  wl-2sb6d  31934  wl-mo2df  31945  wl-mo2t  31950  wl-ax12v3  31958  poimirlem2  31988  poimirlem25  32011  poimirlem28  32014  poimirlem31  32017  heicant  32021  mbfresfi  32033  itg2gt0cn  32043  sdclem2  32117  fdc  32120  seqpo  32122  incsequz  32123  mettrifi  32132  prdsbnd2  32173  heiborlem4  32192  bfplem1  32200  iscringd  32278  maxidlval  32318  igenval2  32345  ax12eq  32558  ax12el  32559  ax12indalem  32562  ax12inda2ALT  32563  ax12inda  32565  ax12v2-o  32566  riotasvd  32574  isopos  32792  isat3  32919  ishlat1  32964  glbconN  32988  ispsubsp  33356  isldil  33721  isltrn  33730  isdilN  33766  trlval  33774  cdleme27b  33981  cdleme29b  33988  cdleme31sn1  33994  cdleme31sn1c  34001  cdleme40v  34082  cdlemk36  34526  cdlemkid5  34548  cdlemn11pre  34824  dihord2pre  34839  islpolN  35097  hdmapffval  35443  hdmapfval  35444  hdmapval2lem  35448  ismrc  35589  incssnn0  35599  mzpexpmpt  35633  pell14qrexpclnn0  35758  monotuz  35835  expmordi  35841  rmxypos  35843  jm2.17a  35856  jm2.17b  35857  rmygeid  35860  divalgmodcl  35888  jm2.18  35889  jm2.19lem3  35892  jm2.25  35900  jm2.15nn0  35904  jm2.16nn0  35905  wepwsolem  35946  aomclem8  35965  dfac11  35966  pwslnm  35998  lnr2i  36021  hbtlem5  36033  cnsrexpcl  36077  rngunsnply  36085  isdomn3  36127  ifpbi23  36162  elmapintrab  36228  elmapintab  36248  cnvcnvintabd  36252  eliunov2  36317  relexpxpnnidm  36341  relexpiidm  36342  relexpss1d  36343  iunrelexpmin1  36346  relexpmulnn  36347  iunrelexpmin2  36350  relexp0a  36354  trclimalb2  36364  dvgrat  36706  pm14.122b  36819  fnchoice  37391  fiiuncl  37445  wessf1ornlem  37513  fperiodmullem  37596  fmul01  37744  fmuldfeq  37747  climsuselem1  37772  climinff  37776  climinffOLD  37777  ellimcabssub0  37783  limcleqr  37811  addlimc  37815  0ellimcdiv  37816  limclner  37818  dvnmptdivc  37899  dvnmptconst  37902  dvnmul  37904  iblspltprt  37936  itgspltprt  37942  stoweidlem2  37963  stoweidlem3  37964  stoweidlem17  37978  stoweidlem19  37980  stoweidlem21  37982  stoweidlem26  37987  fourierdlem42  38113  fourierdlem42OLD  38114  issal  38276  ismea  38394  isome  38423  carageniuncllem1  38450  caratheodorylem1  38455  smonoord  38853  perfectALTVlem2  38979  2ffzoeq  39202  usgra2pth  40037  usgfis  40127  lmodvsmdi  40536  dmatALTval  40562  dmatALTbasel  40564  snlindsntor  40633  ldepsnlinc  40670  elbigo2r  40733  elbigolo1  40737