Theorem imbi2d 308

Description: Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-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 23	. 2 |- ( ph -> ( th -> ( ps <-> ch ) ) )
3	2	pm5.74d 239	1 |- ( ph -> ( ( th -> ps ) <-> ( th -> ch ) ) )

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

This theorem is referenced by:  imbi12d  312  imbi2  315  pm5.42  532  orbi2d  683  con3th  925  19.23tOLD  1834  ax12olem6OLD  1982  ax11v2  2045  ax15  2070  nfsb4t  2129  sbcom  2138  ax11vALT  2146  sbcom2  2163  ax11eq  2243  ax11el  2244  ax11indalem  2247  ax11inda2ALT  2248  ax11inda  2250  ax11v2-o  2251  mo  2276  2mo  2332  2eu6  2339  2gencl  2945  3gencl  2946  vtocl2gf  2973  vtocl3gf  2974  eqeu  3065  mo2icl  3073  euind  3081  reu7  3089  reuind  3097  sbctt  3183  sbcnestgf  3258  r19.36zv  3688  dedth2h  3741  dedth3h  3742  dedth4h  3743  preq12bg  3937  elint  4016  elintrabg  4023  intab  4040  trss  4271  axrep1  4281  axrep2  4282  axrep3  4283  bm1.3ii  4293  pocl  4470  swopolem  4472  solin  4486  freq1  4512  frminex  4522  reusv3  4690  tfisi  4797  tfindsg  4799  tfinds2  4802  tfinds3  4803  dfom2  4806  elom  4807  findsg  4831  finds2  4832  vtoclr  4881  2optocl  4912  3optocl  4913  raliunxp  4973  resieq  5115  iss  5148  cnveqb  5285  funmo  5429  funimaexg  5489  fnbrfvb  5726  fvelimab  5741  fvmptss  5772  fmptco  5860  fprg  5874  fnressn  5877  fressnfv  5879  isoselem  6020  ovg  6171  caovcan  6210  caovordig  6211  caovord  6217  f1o2ndf1  6413  poxp  6417  fnse  6422  riotasvd  6551  riotasvdOLD  6552  smoeq  6571  smores  6573  smogt  6588  tfrlem1  6595  tfr3  6619  oaordi  6748  oeordi  6789  oeoa  6799  oeoe  6801  nnacl  6813  nnmcl  6814  nnecl  6815  nnacom  6819  nnaordi  6820  nnawordi  6823  nnaass  6824  nndi  6825  nnmass  6826  nnmsucr  6827  nnmcom  6828  nnmordi  6833  2ecoptocl  6954  3ecoptocl  6955  th3qlem2  6970  undifixp  7057  xpdom2g  7163  findcard2  7307  xpfi  7337  fnfi  7343  fodomfi  7344  finsschain  7371  marypha1lem  7396  marypha1  7397  supeq1  7408  ordiso2  7440  ordtypelem7  7449  wemaplem1  7471  inf3lem2  7540  inf3lem5  7543  infdiffi  7568  cantnfval2  7580  cantnfle  7582  cantnfp1lem3  7592  oemapval  7595  cantnflem1  7601  cantnf  7605  wemapwe  7610  cnfcom  7613  cnfcom3clem  7618  tz9.1  7621  r1pwOLD  7728  cplem2  7770  karden  7775  infxpenc2lem2  7857  fseqenlem1  7861  dfac8clem  7869  alephinit  7932  dfac4  7959  dfac5lem5  7964  dfac2a  7966  dfac2  7967  dfacacn  7977  dfac12lem3  7981  kmlem2  7987  kmlem13  7998  ackbij1lem16  8071  sornom  8113  infpssrlem4  8142  fin23lem14  8169  fin23lem32  8180  fin23lem34  8182  fin23lem36  8184  isf32lem1  8189  isf32lem2  8190  axcc2lem  8272  axcc3  8274  axcclem  8293  zornn0g  8341  ttukeylem5  8349  ttukeylem6  8350  axrepnd  8425  axpowndlem3  8430  zfcndrep  8445  fpwwe2lem8  8468  pwfseqlem3  8491  wunr1om  8550  wunfi  8552  tskr1om  8598  ingru  8646  grudomon  8648  axgroth3  8662  axgroth4  8663  nqereu  8762  mulcanenq  8793  elnp  8820  elnpi  8821  prlem934  8866  infm3  9923  nnaddcl  9978  nnmulcl  9979  peano5uzi  10314  uzind2  10318  uzindOLD  10320  zindd  10327  eluzadd  10470  uzaddcl  10489  uzwo  10495  uzwoOLD  10496  indstr  10501  zmax  10527  xmulasslem  10820  xrsupsslem  10841  xrinfmsslem  10842  xrsupss  10843  xrinfmss  10844  flval2  11176  om2uzlti  11245  uzrdgfni  11253  seqcl2  11296  seqfveq2  11300  seqshft2  11304  monoord  11308  seqsplit  11311  seqcaopr3  11313  seqf1olem2a  11316  seqf1o  11319  seqid2  11324  seqhomo  11325  ser1const  11334  expcllem  11347  expeq0  11365  mulexp  11374  expadd  11377  expmul  11380  leexp2r  11392  leexp1a  11393  bernneq  11460  modexp  11469  facdiv  11533  faclbnd  11536  faclbnd4lem4  11542  faclbnd6  11545  hashgadd  11606  hashxp  11652  hashmap  11653  hashf1lem2  11660  hashf1  11661  seqcoll  11667  wrdind  11746  cjexp  11910  absexp  12064  rlim  12244  rlim2  12245  rlim0  12257  rlim0lt  12258  rlimi  12262  ello12r  12266  ello1mpt  12270  ello1d  12272  elo12r  12277  lo1o1  12281  o1lo1  12286  lo1res  12308  climshft  12325  o1compt  12336  rlimo1  12365  lo1add  12375  lo1mul  12376  rlimdiv  12394  climub  12410  climserle  12411  caucvgrlem  12421  caurcvgr  12422  iseraltlem2  12431  summolem2a  12464  sumss  12473  fsum2d  12510  fsumabs  12535  fsumrlim  12545  fsumo1  12546  fsumiun  12555  binom  12564  bcxmas  12570  climcndslem1  12584  climcndslem2  12585  cvgrat  12615  demoivreALT  12757  ruclem8  12791  ruclem9  12792  dvdsle  12850  dvdsfac  12859  divalglem7  12874  bitsinv1  12909  sadcadd  12925  sadadd2  12927  saddisjlem  12931  smuval2  12949  smupvallem  12950  smu01lem  12952  smupval  12955  smueqlem  12957  smumullem  12959  bezoutlem4  12996  gcdmultiple  13005  rplpwr  13011  nn0seqcvgd  13016  seq1st  13017  alginv  13021  algcvga  13025  algfx  13026  prmind2  13045  prmdvdsexp  13069  prmfac1  13073  pcmpt  13216  pcfac  13223  prmpwdvds  13227  prmreclem4  13242  vdwlem10  13313  ramval  13331  ramcl  13352  prmlem1a  13384  imasleval  13721  ismre  13770  mreexexd  13828  lubprop  14392  lubid  14394  glbprop  14397  joinlem  14402  meetlem  14409  isglbd  14499  lubun  14505  oduclatb  14526  poslubmo  14528  poslubd  14529  spwmo  14613  spwpr4  14618  frmdgsum  14762  mulgnnass  14873  mhmmulg  14877  gsumwrev  15117  sylow1lem1  15187  efginvrel2  15314  efgsrel  15321  efgredlemd  15331  efgredlem  15334  efgred  15335  efgrelexlemb  15337  gsum2d  15501  gsumcom2  15504  ablfac1eulem  15585  pgpfac1lem2  15588  pgpfac1lem5  15592  pgpfac1  15593  pgpfac  15597  isdomn2  16314  mplcoe1  16483  mplcoe3  16484  mplcoe2  16485  cnfldexp  16689  fiinopn  16929  mretopd  17111  neiptoptop  17150  cnpfval  17252  iscnp3  17262  tgcn  17270  lmbr  17276  lmbr2  17277  lmbrf  17278  lmss  17316  ishaus  17340  hausnei2  17371  t1sep2  17387  fiuncmp  17421  dfcon2  17435  1stcfb  17461  2ndc1stc  17467  1stcrest  17469  1stcelcls  17477  1stccn  17479  lly1stc  17512  elkgen  17521  kgencn  17541  tx1stc  17635  xkopt  17640  cnmptcom  17663  isr0  17722  r0sep  17733  ptcmpfi  17798  isfildlem  17842  rnelfm  17938  fbflim  17961  flimrest  17968  isflf  17978  flffbas  17980  lmflf  17990  fclsrest  18009  isfcf  18019  cnextfvval  18049  tmdmulg  18075  tmdgsum  18078  eltsms  18115  tsmsi  18116  tsmsgsum  18121  tsmssubm  18125  tsmsres  18126  tsmsf1o  18127  isust  18186  isucn  18261  isucn2  18262  ucnima  18264  imasdsf1olem  18356  metss  18491  met1stc  18504  metcnp  18524  metcnpi  18527  metcnpi2  18528  metucnOLD  18571  metucn  18572  xrge0tsms  18818  fsumcn  18853  elcncf  18872  cncfi  18877  rescncf  18880  cncfco  18890  caucfil  19189  equivcau  19206  caubl  19213  caublcls  19214  ovolgelb  19329  ovolunlem1a  19345  ovolicc2lem3  19368  voliunlem1  19397  voliunlem3  19399  volsuplem  19402  volsup  19403  dyadmax  19443  vitali  19458  itg2leub  19579  itgfsum  19671  dvnadd  19768  dvnres  19770  cpnord  19774  dvnfre  19791  dvmptfsum  19812  dvferm1  19822  dvferm2  19824  rolle  19827  dvlip  19830  c1lip1  19834  lhop1  19851  deg1leb  19971  ply1divex  20012  fta1g  20043  plyco  20113  dgrcolem1  20144  dgrco  20146  dvnply2  20157  plydivex  20167  aalioulem2  20203  aalioulem3  20204  aalioulem5  20206  aaliou3lem2  20213  dvntaylp  20240  taylthlem1  20242  ulmdvlem3  20271  abelthlem9  20309  cxpmul2  20533  scvxcvx  20777  jensenlem2  20779  jensen  20780  wilthlem3  20806  perfectlem2  20967  bcmono  21014  bposlem5  21025  lgsquad2lem2  21096  dchrisumlem1  21136  dchrisum0flb  21157  pntpbnd1  21233  pntlemf  21252  qabvle  21272  qabvexp  21273  ostthlem2  21275  ostth2lem2  21281  sizeusglecusglem1  21446  2pthoncl  21556  fargshiftf1  21577  3v3e3cycl1  21584  4cycl4v4e  21606  4cycl4dv4e  21608  eupatrl  21643  eupath2  21655  isplig  21718  gxnn0add  21815  gxnn0mul  21818  ghgrp  21909  ghablo  21910  isnvlem  22042  nvi  22046  nmoubi  22226  nmounbi  22230  nmblolbi  22254  ipasslem1  22285  ipassi  22295  hlim2  22647  pjhth  22848  spansni  23012  elspansn2  23022  pjige0  23146  pjcjt2  23147  pjopyth  23175  elcnop  23313  elcnfn  23338  nmopub  23364  cnopc  23369  nmfnleub  23381  elnlfn  23384  cnfnc  23386  nmbdoplb  23481  nmcexi  23482  nmcoplb  23486  lnfnmul  23504  nmbdfnlb  23506  nmcfnlb  23510  pjss2coi  23620  pjssmi  23621  isst  23669  ishst  23670  stcltr1i  23730  mdbr  23750  dmdbr  23755  mddmd2  23765  mdslmd1lem3  23783  mdslmd1lem4  23784  elat2  23796  atcvat2  23845  cdj1i  23889  iuninc  23964  fmptcof2  24029  xrge0tsmsd  24176  isofld  24188  ofldadd  24191  ofldchr  24197  isarchi2  24208  esumfzf  24412  issiga  24447  isrnsiga  24449  ismeas  24506  isrnmeas  24507  measiun  24525  rrvsum  24665  subfacp1lem6  24824  erdszelem8  24837  isscon  24866  cvmliftlem7  24931  cvmliftlem10  24934  cvmlift3lem2  24960  ghomf1olem  25058  relexp0  25082  relexpsucr  25083  relexpsucl  25085  relexpind  25093  dfrtrclrec2  25096  rtrclreclem.refl  25097  rtrclreclem.subset  25098  rtrclreclem.min  25100  dfrtrcl2  25101  shftvalg  25161  clim2prod  25169  prodfn0  25175  prodfrec  25176  ntrivcvgfvn0  25180  prodmolem2a  25213  fprodabs  25250  fprodefsum  25251  fprodn0  25256  fprod2d  25258  iprodefisumlem  25270  binomfallfac  25308  faclimlem1  25310  dfpo2  25326  rdgprc  25365  preddowncl  25410  trpredmintr  25448  frmin  25456  soseq  25468  wfr3g  25469  wfrlem4  25473  frr3g  25494  bpolycl  26002  bpolydif  26005  fveleq  26105  mbfresfi  26152  itg2gt0cn  26159  sdclem2  26336  fdc  26339  seqpo  26341  incsequz  26342  mettrifi  26353  prdsbnd2  26394  heiborlem4  26413  bfplem1  26421  iscringd  26499  maxidlval  26539  igenval2  26566  ismrc  26645  incssnn0  26655  mzpexpmpt  26692  pell14qrexpclnn0  26819  monotuz  26894  expmordi  26900  rmxypos  26902  jm2.17a  26915  jm2.17b  26916  rmygeid  26919  divalgmodcl  26948  jm2.18  26949  jm2.19lem3  26952  jm2.25  26960  jm2.15nn0  26964  jm2.16nn0  26965  wepwsolem  27006  aomclem8  27027  dfac11  27028  pwslnm  27064  islindf4  27176  lnr2i  27188  hbtlem5  27200  cnsrexpcl  27238  rngunsnply  27246  psgnunilem3  27287  isdomn3  27391  pm14.122b  27491  fnchoice  27567  fmul01  27577  fmuldfeq  27580  climsuselem1  27600  climinff  27604  stoweidlem2  27618  stoweidlem3  27619  stoweidlem17  27633  stoweidlem19  27635  stoweidlem21  27637  stoweidlem26  27642  swrdccatin2  28018  swrdccatin12lem4  28025  swrdccatin12  28026  swrdccat3  28029  usgra2pth  28041  el2wlkonot  28066  el2spthonot  28067  frgra3vlem1  28104  3vfriswmgralem  28108  usg2spot2nb  28168  2spotmdisj  28171  bnj941  28849  bnj106  28945  bnj155  28956  bnj590  28987  bnj591  28988  bnj849  29002  bnj893  29005  bnj944  29015  bnj1128  29065  ax12olem6NEW7  29165  ax11v2NEW7  29234  ax15NEW7  29240  nfsb4twAUX7  29280  sbcomwAUX7  29291  nfsb4tOLD7  29429  nfsb4tw2AUXOLD7  29430  sbcomOLD7  29439  sbcom2OLD7  29445  lubunNEW  29456  isopos  29663  isat3  29790  ishlat1  29835  glbconN  29859  ispsubsp  30227  isldil  30592  isltrn  30601  isdilN  30636  trlval  30644  cdleme27b  30850  cdleme29b  30857  cdleme31sn1  30863  cdleme31sn1c  30870  cdleme40v  30951  cdlemk36  31395  cdlemkid5  31417  cdlemn11pre  31693  dihord2pre  31708  islpolN  31966  hdmapffval  32312  hdmapfval  32313  hdmapval2lem  32317

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178