Theorem anbi12d 628

Description: Deduction joining two equivalences to form equivalence of conjunctions.

Hypotheses

Ref	Expression
bi12d.1	|- (ph -> (ps <-> ch))
bi12d.2	|- (ph -> (th <-> ta))

Assertion

Ref	Expression
anbi12d	|- (ph -> ((ps /\ th) <-> (ch /\ ta)))

Proof of Theorem anbi12d

Step	Hyp	Ref	Expression
1		bi12d.1	. . 3 |- (ph -> (ps <-> ch))
2	1	anbi1d 617	. 2 |- (ph -> ((ps /\ th) <-> (ch /\ th)))
3		bi12d.2	. . 3 |- (ph -> (th <-> ta))
4	3	anbi2d 616	. 2 |- (ph -> ((ch /\ th) <-> (ch /\ ta)))
5	2, 4	bitrd 528	1 |- (ph -> ((ps /\ th) <-> (ch /\ ta)))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  pm4.38 631  3anbi123d 893  drsb1 1175  sb7f 1341  mopick 1433  clelab 1580  cbvrex 1797  cbvreuv 1800  gencbvex 1836  rcla4e 1870  eqvincf 1882  ceqsrexv 1887  elrabf 1902  cbvrab 1908  reu2 1928  reu3 1929  rmo4 1931  reu8 1934  sbcang 1969  sbcabel 1994  sbcel12g 2009  eldif 2055  psseq1 2133  psseq2 2134  ssconb 2168  elin 2205  elunii 2506  eluniab 2511  cbvopab 2670  cbvopab1 2672  cbvopab1s 2673  cbvopab2v 2675  nalset 2710  elssabg 2724  intabs 2731  unipw 2754  nnullss 2766  exss 2767  opabid 2808  opelopab2 2817  dfid3 2834  poeq1 2840  pocl 2842  soeq1 2851  axun 2865  fri 2916  frc 2918  weeq1 2935  weeq2 2936  ordeq 2953  onminex 3018  elom 3132  elomg 3133  vtoclr 3209  opbrop 3236  relop 3273  asymref2 3438  elxp4 3451  elxp5 3452  funopg 3545  fununi 3561  funcnvuni 3562  fneq1 3580  2elresin 3596  feq1 3618  fcoi2 3644  f1eq1 3658  foeq1 3666  f1oeq1 3682  f1oeq2 3683  f1oeq3 3684  ffoss 3709  fv3 3731  tz6.12f 3736  fnopabfv 3756  ssimaex 3766  fvopab3 3775  fvopab3ig 3776  fvopab4gf 3779  elunirnALT 3867  isoeq1 3885  isoeq4 3888  isomin 3897  isoini 3898  isofrlem 3899  isowe 3901  f1oweALT 3904  tfrlem1 3909  tfrlem3 3911  tfrlem5 3913  tfrlem12 3920  tz7.44-2 3927  tz7.44-3 3928  rdglem2 3936  cbvoprab12 3996  oprabval 4021  oprabvalig 4022  oprabval2gf 4024  oprabval4g 4029  caoprmo 4068  2ndconst 4095  unielxp 4105  dfoprab5 4113  ertr 4272  ecelqsi 4290  brecop 4304  ecopoprtrn 4309  th3qlem1 4312  th3qlem2 4313  th3q 4315  elpm 4334  elixp2 4347  ixpeq1 4351  mapsnen 4424  xpsnen 4429  endisj 4431  pw2en 4440  sbthlem2 4442  sbth 4451  php2 4508  nnsdomo 4515  unfilem1 4538  unifi 4546  fiint 4548  abfii4 4552  supeq1 4563  supmo 4564  supub 4568  suplub 4569  supmaxlem 4576  suppr 4578  supsnALT 4580  en2lp 4590  inf0 4594  axinf2 4612  dfom3 4618  unbnnt 4627  rankr1g 4663  r1pwcl 4675  karden 4714  aceq1 4717  aceq0 4718  aceq2 4719  aceq3lem 4720  aceq3 4721  aceq4 4722  aceq5lem1 4723  aceq5lem2 4724  aceq5lem3 4725  aceq5lem4 4726  aceq5 4728  aceq6a 4729  aceq6b 4730  axac 4733  ac7g 4737  ac5 4740  ac6lem 4742  kmlem1 4753  kmlem2 4754  kmlem4 4756  kmlem14 4766  zorn2lem1 4776  zorn2lem7 4782  zorn2 4784  brdom3 4789  brdom7disj 4792  brdom6disj 4793  unidom 4796  cardsdom 4825  alephnbtwn2 4857  aleph11 4867  dominf 4892  cflem 4893  cfval 4894  cflecard 4900  cfeq0 4902  cfsuc 4903  axrepndlem2 4933  axunnd 4936  axregndlem2 4943  axinfndlem1 4945  axacndlem5 4951  axacnd 4952  zfcndun 4955  zfcndac 4959  ltsopi 5004  indpi 5022  ltsopq 5063  ltbtwnpq 5072  elnp 5080  prcdpq 5085  genpv 5090  genpprecl 5092  genpnmax 5098  ltprord 5122  ltsopr 5124  ltexprlem4 5133  ltexprlem7 5136  prlem936 5143  reclem1pr 5144  reclem3pr 5146  supexpr 5151  ltsosr 5191  negexsr 5199  recexsr 5204  suppsr 5210  suppsr3 5212  supsrlem5 5217  supsrlem6 5218  ltresr 5246  supre 5248  ltsor 5249  axrnegex 5271  axrrecex 5272  axcnre 5274  ltxrt 5483  axlttrn 5492  axsup 5495  letri3t 5505  ltleaddt 5633  lesub0t 5665  div11t 5736  recrect 5747  prodgt0t 5797  prodge0t 5799  posex 5876  peano5nn 5894  dfnn2 5904  nn2get 5910  nominpos 6011  lbinfm 6016  sup2 6019  infm3 6022  dfinfmr 6035  infmsup 6036  nnunb 6038  xrsupsslem 6044  xrinfmsslem 6045  xrsupss 6046  xrinfmss 6047  supxr 6049  zltp1let 6149  z2get 6156  dfuz 6170  peano5uz 6171  uzind 6173  uzindOLD 6176  zmax 6188  rebtwnz 6190  flvalt 6193  flleltt 6196  flval2t 6205  flbit 6207  flbi2t 6208  quorem 6218  qbtwnre 6242  qbtwnxr 6243  iooint 6336  elioo1t 6342  elioo2t 6343  elioc1t 6346  elico1t 6347  elicc1t 6348  ioonegt 6366  iccnegt 6367  icoshft 6368  icoshftf1olem 6370  icounlem 6372  icoun 6373  nnwof 6419  elfz1t 6430  fzrevt 6471  sqr0 6632  sqrlem4 6636  sqrlem24 6656  sqrgt0i 6657  sqrlem26 6658  sqr2irrlem2 6685  absltt 6838  abslet 6839  absdifltt 6841  absdiflet 6842  abs1m 6862  abs3lemt 6865  cau3ir 6873  cau5i 6875  bcvalt 6916  clim 6935  dffsum 6956  climuni 7057  climshft 7062  climres 7063  iserzshft2 7065  climrecl 7068  climge0 7070  caucvg3t 7126  cvgcmp3cetlem1 7146  cvgcmp3cetlem2 7147  iserzgt0 7169  expcnvlem5 7189  geolim 7195  geolim1 7197  fsum0diag 7216  cncfval 7222  elcncf 7223  efseq1ex 7264  absef01tlub 7346  efcnlem4 7379  reeff1olem2 7382  acdc3 7444  acdc2 7447  acdc5 7450  acdc 7452  infpnlem2 7464  infpn2 7466  ruclem4 7470  ruclem12 7478  ruclem29 7495  ruclem36 7502  infxpidmlem2 7510  infxpidmlem3 7511  infxpidmlem8 7516  infpss 7531  infmap2lem1 7536  istopg 7553  eltopsp 7561  tpsex 7562  istps 7563  eltg2t 7576  tgval3t 7582  topbast 7584  subbas 7601  subtop 7603  fctop 7607  cctop 7609  retopbas 7612  cldval 7623  ntrfval 7624  clsfval 7625  iscld 7626  elcls 7661  neifval 7671  isnei 7675  neiint 7676  neips 7684  opnneissb 7685  opnssneib 7686  innei 7693  lpfval 7699  islp2 7704  qdensere 7708  cnpfval 7714  ismet 7755  dfms2 7756  ismsg 7757  msflem 7760  metreslem 7779  blfval 7792  blelrn 7805  blin 7809  blss 7810  blssex 7811  opnfval 7814  opnm 7817  blssopn 7824  opnin 7826  neibl 7834  blnei 7836  metcnp 7844  metcn 7846  metcnpi3 7849  metcnpi4 7850  metcni2 7852  tgioolem 7871  caufval 7883  lmbr 7885  iscau3 7895  iscau4 7897  lmss 7910  lmfex 7916  lmle 7917  metelcls 7922  metcnp4 7927  xpcn 7933  fsumcnlem 7946  iscms2lem4 7949  lmcau 7953  bcthlem2 7957  bcthlem7 7962  bcthlem15 7970  bcth 7989  isgrp 7998  isgrpi 7999  grpideu 8010  grpidinv2 8017  grpinvfval 8023  grpinv 8026  grpdivfval 8038  isring 8098  ringi 8099  ringid 8102  cnring 8119  ringsn 8120  vci 8124  isvclem 8153  nmcnilem 8294  va1cnlem 8302  sm1cnilem 8304  ipfval 8309  lnoval 8370  islno 8371  nmofval 8382  nmosetn0 8385  nmolb 8391  nmlno0lem 8410  blocni 8422  ajmoi 8476  pslem 8604  spwval2 8610  spwmo 8613  spwpr2 8615  spwpr3OLD 8619  spwpr4OLD 8620  spwpr4aOLD 8621  pilem2 8629  pilem3 8630  pilem4 8631  sinperlem2 8644  sincosq1sgn 8661  sincosq2sgn 8662  sincosq3sgn 8663  sincosq4sgn 8664  efifolem2 8678  efifolem3 8679  efifolem6 8682  effoi 8700  normlem7tALT 8940  norm3lemt 8974  hcau 9006  hcau2 9010  hlim 9011  hlim2 9015  sh 9033  closedsub 9048  chlim 9059  hlimuni 9064  ch2 9069  hhsssh 9094  ocsh 9111  ocin 9124  projlem7 9147  projlem17 9157  projlem26 9166  projlem28 9168  pjtheut 9191  pjmvalt 9193  omls 9201  pjomlt 9224  shintclt 9249  chintclt 9251  shlubt 9309  chpsscon3t 9381  cmbrt 9482  pjoml6 9487  cm2jt 9518  spansncvt 9553  pjrn 9602  adjmo 9713  eigret 9716  eigortht 9719  elcnopt 9738  ellnopt 9739  nmopsetn0 9747  elunopt 9754  elhmopt 9755  nmfnsetn0 9760  elcnfnt 9764  ellnfnt 9765  eigvalvalt 9778  nmoplbt 9786  nmfnlbt 9803  eleigvect 9836  0cnop 9858  0cnfn 9859  idcnop 9860  nmlnop0ALT 9875  lnophmt 9899  lnopcon 9918  nmbdfnlbt 9934  lnfncon 9945  branmfnt 9993  bra11 9996  leopg 10010  leoptrit 10024  leoptrt 10025  hmopidmcht 10036  hmopidmpjt 10037  elpjrncht 10073  stelt 10096  hstelt 10097  hstel2t 10101  jp 10152  cvbrt 10164  cvcon3t 10166  cvnbtwnt 10168  mdbrt 10176  dmdbrt 10181  mdsl1 10203  mdslmd1lem3 10209  mdslmd1lem4 10210  csmdsym 10216  elat2 10222  chrelat 10246  chrelat2 10247  cvexchlem 10250  irredt 10277  atcvat4 10279  mdsymlem2 10286  mdsymlem8 10292  mddmdin0 10313  cdj1 10315  cdj3 10323  elghomlem1 10337  elghomlem2 10338  cbvrexf 10392  abfi 10403  ficli 10422  iseuctopg 10444  hmeogrp 10480  qusp 10485  isfil 10488  cnfilca 10506  rcfpfillem3 10509  sfvlim 10518  trnij 10549  cnvtr 10550  ismgra 10554  isalg 10565  algi 10572  isded 10581  dedi 10582  idosd 10589  iscat 10599  cati 10600  cmpasso 10618  ishomd 10630  ismona 10647  ismonb 10648  imonclem 10651  isfuna 10660  isfunb 10661  ishgrag 10674  hgralem 10675  ispgrag 10684

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain