Theorem anbi12d 626

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 615	. 2 |- (ph -> ((ps /\ th) <-> (ch /\ th)))
3		bi12d.2	. . 3 |- (ph -> (th <-> ta))
4	3	anbi2d 614	. 2 |- (ph -> ((ch /\ th) <-> (ch /\ ta)))
5	2, 4	bitrd 526	1 |- (ph -> ((ps /\ th) <-> (ch /\ ta)))

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

This theorem is referenced by:  pm4.38 629  3anbi123d 890  drsb1 1171  sb7f 1336  mopick 1426  clelab 1573  cbvrex 1790  cbvreuv 1793  gencbvex 1829  rcla4e 1863  eqvincf 1875  ceqsrexv 1880  elrabf 1895  cbvrab 1901  reu2 1920  reu3 1921  rmo4 1923  reu8 1926  sbcang 1961  sbcabel 1986  sbcel12g 2001  eldif 2047  psseq1 2125  psseq2 2126  ssconb 2160  elin 2197  elunii 2498  eluniab 2503  cbvopab 2662  cbvopab1 2664  cbvopab1s 2665  cbvopab2v 2667  nalset 2702  elssabg 2716  intabs 2723  unipw 2746  nnullss 2758  exss 2759  opabid 2799  opelopab2 2808  dfid3 2826  poeq1 2833  pocl 2835  soeq1 2844  axun 2858  fri 2908  frc 2910  weeq1 2927  weeq2 2928  ordeq 2945  onminex 3010  elom 3124  elomg 3125  vtoclr 3201  opbrop 3228  relop 3265  asymref2 3424  asymref2OLD 3426  elxp4 3439  elxp5 3440  funopg 3533  fununi 3549  funcnvuni 3550  fneq1 3568  2elresin 3584  feq1 3606  fcoi2 3631  f1eq1 3645  foeq1 3653  f1oeq1 3669  f1oeq2 3670  f1oeq3 3671  ffoss 3696  fv3 3718  tz6.12f 3723  fnopabfv 3743  ssimaex 3753  fvopab3 3762  fvopab3ig 3763  fvopab4gf 3766  elunirnALT 3854  isoeq1 3872  isoeq4 3875  isomin 3884  isoini 3885  isofrlem 3886  isowe 3888  f1oweALT 3891  tfrlem1 3896  tfrlem3 3898  tfrlem5 3900  tfrlem12 3907  tz7.44-2 3914  tz7.44-3 3915  rdglem2 3923  cbvoprab12 3983  oprabval 4008  oprabvalig 4009  oprabval2gf 4011  oprabval4g 4016  caoprmo 4056  2ndconst 4081  unielxp 4091  dfoprab5 4099  ertr 4258  ecelqsi 4276  brecop 4290  ecopoprtrn 4295  th3qlem1 4298  th3qlem2 4299  th3q 4301  elpm 4320  elixp2 4333  ixpeq1 4337  mapsnen 4410  xpsnen 4415  endisj 4417  pw2en 4426  sbthlem2 4428  sbth 4437  php2 4494  nnsdomo 4501  unfilem1 4524  unifi 4532  fiint 4534  abfii4 4538  supeq1 4549  supmo 4550  supub 4554  suplub 4555  suppr 4562  supsnALT 4564  en2lp 4574  inf0 4578  axinf2 4596  dfom3 4602  unbnnt 4611  rankr1g 4647  r1pwcl 4659  karden 4698  aceq1 4701  aceq0 4702  aceq2 4703  aceq3lem 4704  aceq3 4705  aceq4 4706  aceq5lem1 4707  aceq5lem2 4708  aceq5lem3 4709  aceq5lem4 4710  aceq5 4712  aceq6a 4713  aceq6b 4714  axac 4717  ac7g 4721  ac5 4724  ac6lem 4726  kmlem1 4737  kmlem2 4738  kmlem4 4740  kmlem14 4750  zorn2lem1 4760  zorn2lem7 4766  zorn2 4768  brdom3 4773  brdom7disj 4776  brdom6disj 4777  unidom 4780  cardsdom 4809  alephnbtwn2 4841  aleph11 4851  dominf 4876  cflem 4877  cfval 4878  cflecard 4884  cfeq0 4886  cfsuc 4887  axrepndlem2 4917  axunnd 4920  axregndlem2 4927  axinfndlem1 4929  axacndlem5 4935  axacnd 4936  zfcndun 4939  zfcndac 4943  ltsopi 4988  indpi 5006  ltsopq 5047  ltbtwnpq 5056  elnp 5064  prcdpq 5069  genpv 5074  genpprecl 5076  genpnmax 5082  ltprord 5106  ltsopr 5108  ltexprlem4 5117  ltexprlem7 5120  prlem936 5127  reclem1pr 5128  reclem3pr 5130  supexpr 5135  ltsosr 5175  negexsr 5183  recexsr 5188  suppsr 5194  suppsr3 5196  supsrlem5 5201  supsrlem6 5202  ltresr 5230  supre 5232  ltsor 5233  axrnegex 5255  axrrecex 5256  axcnre 5258  ltxrt 5467  axlttrn 5476  axsup 5479  letri3t 5490  ltleaddt 5619  lesub0t 5651  div11t 5721  recrect 5732  prodgt0t 5782  prodge0t 5784  posex 5856  peano5nn 5874  dfnn2 5884  nn2get 5890  nominpos 5990  lbinfm 5995  sup2 5998  infm3 6001  dfinfmr 6014  infmsup 6015  nnunb 6017  xrsupsslem 6023  xrinfmsslem 6024  xrsupss 6025  xrinfmss 6026  supxr 6028  zltp1let 6128  z2get 6135  dfuz 6150  peano5uz 6151  uzind 6153  uzindOLD 6156  zmax 6168  rebtwnz 6170  flvalt 6173  flleltt 6175  flval2t 6181  flbit 6184  qbtwnre 6216  qbtwnxr 6217  iooint 6309  elioo1t 6315  elioo2t 6316  elioc1t 6319  elico1t 6320  elicc1t 6321  ioonegt 6339  iccnegt 6340  icoshft 6341  icoshftf1olem 6343  icounlem 6345  icoun 6346  nnwof 6391  elfz1t 6402  fzrevt 6443  sqr0 6602  sqrlem4 6606  sqrlem24 6626  sqrgt0i 6627  sqrlem26 6628  sqr2irrlem2 6655  absltt 6817  abslttOLD 6818  abslet 6819  absdifltt 6821  absdiflet 6822  abs1m 6841  abs3lemt 6844  cau3ir 6852  cau5i 6854  bcvalt 6895  clim 6915  dffsum 6936  climuni 7036  climshft 7041  climres 7042  iserzshft2 7044  climrecl 7047  climge0 7049  caucvg3t 7104  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  iserzgt0 7146  expcnvlem5 7166  geolim 7172  geolim1 7174  fsum0diag 7193  cncfval 7199  elcncf 7200  efseq1ex 7248  absef01tlub 7329  efcnlem4 7362  reeff1olem2 7365  reeff1olem2OLD 7367  acdc3 7429  acdc2 7432  acdc5 7435  acdc 7437  infpnlem2 7450  infpn2 7452  ruclem4 7456  ruclem12 7464  ruclem29 7481  ruclem36 7488  infxpidmlem2 7496  infxpidmlem3 7497  infxpidmlem8 7502  infmap2lem1 7521  istopg 7538  eltopsp 7546  tpsex 7547  istps 7548  eltg2t 7561  tgval3t 7567  topbast 7569  subbas 7586  subtop 7588  fctop 7592  cctop 7594  retopbas 7597  cldval 7608  ntrfval 7609  clsfval 7610  iscld 7611  elcls 7646  neifval 7655  isnei 7659  neiint 7660  neips 7668  opnneissb 7669  opnssneib 7670  innei 7677  lpfval 7683  islp2 7688  qdensere 7691  cnpfval 7697  ismet 7737  dfms2 7738  ismsg 7739  msflem 7742  metreslem 7762  blfval 7775  blelrn 7788  blin 7792  blss 7793  blssex 7794  opnfval 7797  opnm 7800  blssopn 7807  opnin 7809  neibl 7817  blnei 7818  metcnp 7826  metcn 7828  metcnpi3 7831  metcnpi4 7832  metcni2 7834  tgioolem 7853  caufval 7864  lmbr 7866  iscau3 7876  lmss 7888  lmfex 7894  lmle 7895  metelcls 7900  metcnp4 7904  xpcn 7910  fsumcnlem 7923  iscms2lem4 7926  lmcau 7930  bcthlem2 7934  bcthlem7 7939  bcthlem15 7947  bcth 7966  isgrp 7975  isgrpi 7976  grpideu 7987  grpidinv2 7994  grpinvfval 8000  grpinv 8003  grpdivfval 8016  isring 8078  ringi 8079  ringid 8082  cnring 8099  ringsn 8100  vci 8104  isvcgOLD 8133  isvclem 8134  nmcnilem 8272  va1cnlem 8279  sm1cnilem 8281  ipfval 8286  lnoval 8347  islno 8348  nmofval 8357  nmosetn0 8360  nmolb 8366  nmlno0lem 8385  blocni 8396  ajmoi 8450  pslem 8573  spwval2 8577  spwmo 8580  pilem2 8591  pilem3 8592  pilem4 8593  sinperlem2 8606  sincosq1sgn 8621  sincosq2sgn 8622  sincosq3sgn 8623  sincosq4sgn 8624  efifolem2 8638  efifolem3 8639  efifolem6 8642  effoi 8666  effoiOLD 8667  normlem7tALT 8906  norm3lemt 8940  hcau 8972  hcau2 8976  hlim 8977  hlim2 8981  sh 8999  closedsub 9014  chlim 9025  hlimuni 9030  ch2 9035  hhsssh 9059  ocsh 9072  ocin 9085  projlem7 9108  projlem17 9118  projlem26 9127  projlem28 9129  pjtheut 9151  pjmvalt 9153  omls 9161  pjomlt 9184  shintclt 9209  chintclt 9211  shlubt 9269  chpsscon3t 9341  cmbrt 9444  pjoml6 9449  cm2jt 9480  spansncvt 9515  pjrn 9564  adjmo 9675  eigret 9678  eigortht 9681  elcnopt 9700  ellnopt 9701  nmopsetn0 9709  elunopt 9716  elhmopt 9717  nmfnsetn0 9722  elcnfnt 9726  ellnfnt 9727  eigvalvalt 9740  nmoplbt 9748  nmfnlbt 9764  eleigvect 9797  0cnop 9819  0cnfn 9820  idcnop 9821  nmlnop0ALT 9835  lnophmt 9859  lnopcon 9878  nmbdfnlbt 9894  lnfncon 9905  branmfnt 9951  bra11 9954  leopg 9967  leoptrit 9981  hmopidmcht 9992  hmopidmpjt 9993  elpjrncht 10028  stelt 10051  hstelt 10052  hstel2t 10056  jp 10107  cvbrt 10119  cvcon3t 10121  cvnbtwnt 10123  mdbrt 10131  dmdbrt 10136  mdsl1 10156  mdslmd1lem3 10162  mdslmd1lem4 10163  csmdsym 10169  elat2 10175  chrelat 10199  chrelat2 10200  cvexchlem 10203  irredt 10230  atcvat4 10232  mdsymlem2 10239  mdsymlem8 10245  mddmdin0 10263  cdj1 10265  cdj3 10273  elghomlem1 10287  elghomlem2 10288  cbvrexf 10338  abfi 10349  ficli 10368  iseuctopg 10389  hmeogrp 10425  qusp 10430  isfil 10433  cnfilca 10451  trnij 10481  cnvtr 10482  ismgra 10486  isalg 10497  algi 10504  isded 10513  dedi 10514  idosd 10521  iscat 10531  cati 10532  cmpasso 10550  ishomd 10562  ismona 10579  ismonb 10580  imonclem 10583  isfuna 10592  isfunb 10593  ishgrag 10605  hgralem 10606  ispgrag 10615

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