Theorem anbi12d 631

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

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221

This theorem is referenced by:  pm4.38 634  3anbi123d 899  drsb1 1212  sb7f 1380  mopick 1472  clelab 1624  cbvrexf 1843  cbvrex 1845  cbvreuv 1848  gencbvex 1884  rcla4e 1918  eqvincf 1930  ceqsrexv 1935  elrabf 1950  cbvrab 1956  reu2 1976  reu3 1977  rmo4 1979  reu8 1982  cbvsbcv 2005  sbcang 2019  sbcabel 2046  sbcel12g 2062  eldif 2109  psseq1 2187  psseq2 2188  ssconb 2222  elin 2259  elunii 2574  eluniab 2579  cbvopab 2746  cbvopab1 2748  cbvopab1s 2749  cbvopab2v 2751  nalset 2786  elssabg 2800  intabs 2807  nnullss 2846  exss 2847  opabid 2887  opelopab2 2896  dfid3 2914  poeq1 2920  pocl 2922  posn 2928  soeq1 2932  fri 2948  frc 2950  weeq1 2964  weeq2 2965  ordeq 2982  zfun 3090  snnex 3100  onminex 3164  elom 3221  elomg 3222  vtoclr 3294  opbrop 3324  relop 3365  asymref2 3532  elxp4 3585  elxp5 3586  funopg 3652  fununi 3668  funcnvuni 3669  fneq1 3688  2elresin 3704  iunfopab 3719  feq1 3727  fcoi2 3753  f1eq1 3767  foeq1 3775  f1oeq1 3792  f1oeq2 3793  f1oeq3 3794  ffoss 3822  fv3 3844  tz6.12f 3849  dffn5 3869  ssimaex 3879  fvopab3 3888  fvopab3ig 3889  fvopab4gf 3892  fvopab6 3905  elunirnALT 3983  isoeq1 4001  isoeq4 4004  isomin 4013  isoini 4014  isofrlem 4015  isowe 4017  f1oweALT 4020  cbvoprab1 4057  cbvoprab12 4058  oprabval 4083  oprabvalig 4084  oprabval2gf 4086  oprabval4g 4091  oprabval4gALT 4092  caoprmo 4131  unielxp 4167  dfoprab4s 4176  dfoprab5sf 4178  tfrlem1 4212  tfrlem3 4214  tfrlem5 4216  tfrlem12 4223  tz7.44-2 4230  tz7.44-3 4231  rdglem2 4239  oeoa 4360  oeoe 4362  ertr 4414  brecop 4447  ecopoprtrn 4452  th3qlem1 4455  th3qlem2 4456  th3q 4458  elpm 4477  elixp2 4490  ixpeq1 4494  mapsnen 4570  xpsnen 4576  endisj 4578  pw2en 4587  ac6sfi 4591  sbthlem2 4593  sbth 4602  php2 4661  nnsdomo 4668  xpfi 4685  unfilem1 4694  unifi 4701  fiint 4703  abfii4 4707  supeq1 4718  supmo 4719  supub 4723  suplub 4724  supmaxlem 4731  suppr 4733  supsnALT 4735  en2lp 4747  inf0 4751  axinf2 4769  dfom3 4776  unbnn3 4785  rankr1g 4821  r1pwcl 4833  karden 4872  aceq1 4875  aceq0 4876  aceq2 4877  aceq3lem 4878  aceq3 4879  aceq4 4880  aceq5lem1 4881  aceq5lem2 4882  aceq5lem3 4883  aceq5lem4 4884  aceq5 4886  aceq6a 4887  aceq6b 4888  zfac 4891  ac7g 4895  ac5 4898  ac6lem 4900  kmlem1 4911  kmlem2 4912  kmlem4 4914  kmlem14 4924  zorn2lem1 4934  zorn2lem7 4940  zorn2 4942  brdom3 4947  brdom7disj 4950  brdom6disj 4951  unidom 4954  cardsdom 4986  alephnbtwn2 5019  aleph11 5029  dominf 5054  cflem 5055  cfval 5056  cflecard 5062  cfeq0 5064  cfsuc 5065  axrepndlem2 5099  axunnd 5102  axregndlem2 5109  axinfndlem1 5111  axacndlem5 5117  axacnd 5118  zfcndun 5121  zfcndac 5125  ltsopi 5170  indpi 5188  ltsopq 5229  ltbtwnpq 5238  elnp 5246  prcdpq 5251  genpv 5256  genpprecl 5258  genpnmax 5264  ltprord 5288  ltsopr 5290  ltexprlem4 5299  ltexprlem7 5302  prlem936 5309  reclem1pr 5310  reclem3pr 5312  supexpr 5317  ltsosr 5357  negexsr 5365  recexsr 5370  suppsr 5376  suppsr3 5378  supsrlem5 5383  supsrlem6 5384  ltresr 5412  supre 5414  ltsor 5415  axrnegex 5437  axrrecex 5438  axcnre 5440  ltxr 5649  axlttrn 5658  axsup 5661  letri3 5671  ltleadd 5799  lesub0 5832  div11 5904  recrec 5915  prodgt0 5966  prodge0 5968  posexi 6053  peano5nni 6071  dfnn2 6081  nn2ge 6087  nominpos 6189  lbinfm 6216  sup2 6219  infm3 6222  dfinfmr 6235  infmsup 6236  nnunb 6238  xrsupsslem 6244  xrinfmsslem 6245  xrsupss 6246  xrinfmss 6247  supxr 6249  zltp1le 6349  z2ge 6359  dfuzi 6373  peano5uzi 6374  uzind 6376  uzindOLD 6379  zmax 6392  rebtwnz 6394  qbtwnre 6418  qbtwnxr 6419  flval 6423  fllelt 6426  flval2 6437  flbi 6439  flbi2 6440  modid2 6472  iooin 6498  elioo1 6504  elioo2 6505  elioc1 6507  elico1 6508  elicc1 6509  iooshf 6522  iooneg 6533  iccneg 6534  icoshft 6535  icoshftf1olem 6537  icounlem 6539  icoun 6540  nnwof 6586  elfz1 6598  fzsuc 6636  fzrev 6642  sqr0 6873  sqrlem4 6877  sqrlem24 6897  sqrgt0ii 6898  sqrlem26 6899  sqr2irrlem2 6926  abslt 7083  absle 7084  absdiflt 7086  absdifle 7087  abs1mi 7107  abs3lem 7110  cau3iri 7118  cau5ii 7120  bcval 7161  clim 7180  dffsum 7201  climuni 7302  climshfti 7307  climresi 7308  iserzshft2i 7310  climrecl 7313  climge0 7315  caucvg3 7371  cvgcmp3cetlem1 7392  cvgcmp3cetlem2 7393  iserzgt0 7415  expcnvlem5 7435  explecnv 7438  geolim 7442  geolim1 7444  fsum0diag 7463  cncfval 7469  elcncf 7470  efseq1ex 7511  absef01tlubi 7593  efcnlem4 7630  reeff1olem2 7633  acdc3 7698  acdc2 7702  acdc5 7705  acdc 7707  infpnlem2 7719  infpn2 7721  ruclem4 7725  ruclem12 7733  ruclem29 7750  ruclem36 7757  infxpidmlem2 7765  infxpidmlem3 7766  infxpidmlem8 7771  infpss 7786  infmap2lem1 7791  istopg 7808  eltopsp 7816  tpsex 7817  istps 7818  eltg2 7831  tgval3 7837  topbas 7839  subbas 7856  subtop 7858  cctop 7862  retopbas 7865  cldval 7876  ntrfval 7877  clsfval 7878  iscld 7879  elcls 7914  neifval 7924  isnei 7928  neiint 7929  neips 7937  opnneissb 7938  opnssneib 7939  innei 7946  lpfval 7952  islp2 7957  qdensere 7961  cnpfval 7967  ismet 8008  dfms2 8009  ismsg 8010  msflem 8013  metreslem 8032  blfval 8045  blelrn 8058  blin 8062  blss 8063  blssex 8064  opnfval 8067  opnm 8070  blssopn 8077  opnin 8079  neibl 8087  blnei 8089  metcnp 8098  metcn 8100  metcnpi3 8103  metcnpi4 8104  metcni2 8106  tgioolem 8125  caufval 8137  lmbr 8139  iscau3 8149  iscau4 8151  lmss 8164  lmfex 8170  lmle 8171  metelcls 8176  metcnp4 8181  xpcn 8187  fsumcnlem 8200  iscms2lem4 8203  lmcau 8207  bcthlem2 8211  bcthlem7 8216  bcthlem15 8224  bcth 8243  isgrp 8254  isgrpi 8255  grpideu 8266  grpidvallem 8274  grpidval 8275  grpidinv2 8277  grpinvfval 8283  grpinv 8286  grpdivfval 8299  gxoprval 8313  isring 8382  ringi 8383  ringid 8386  ringideu 8387  cnring 8404  ringsn 8405  drngi 8408  vci 8414  isvclem 8443  vacnlem3 8584  vacnlem6 8587  vacn 8588  nmcnilem 8591  va1cnlem 8599  sm1cnilem 8601  ipfval 8606  lnoval 8667  islno 8668  nmofval 8679  nmosetn0 8682  nmolb 8688  nmounbseqi 8694  nmlno0lem 8708  blocni 8720  ajmoi 8775  pslem 8909  spwval2 8915  spwmo 8918  spwpr2 8920  spwpr4 8925  spwpr4OLD 8926  spwpr4aOLD 8927  isla 8929  pilem2 8939  pilem3 8940  pilem4 8941  sinperlem2 8954  sincosq1sgn 8971  sincosq2sgn 8972  sincosq3sgn 8973  sincosq4sgn 8974  efifolem2 8995  efifolem3 8996  efifolem6 8999  effoi 9017  normlem7tALT 9261  norm3lemt 9295  hcau 9327  hcau2 9331  hlimi 9332  hlim2 9336  sh 9354  closedsub 9369  chlimi 9380  hlimunii 9385  ch2 9390  hhsssh 9415  ocsh 9432  ocin 9445  projlem7 9468  projlem17 9478  projlem26 9487  projlem28 9489  pjtheu 9512  pjmval 9514  omlsi 9522  pjoml 9545  shintcl 9570  chintcl 9572  shlub 9630  chpsscon3 9702  cmbr 9803  pjoml6i 9808  cm2j 9839  spansncv 9876  pjrni 9925  adjmo 10038  eigre 10041  eigorth 10044  elcnop 10063  ellnop 10064  nmopsetn0 10072  elunop 10079  elhmop 10080  nmfnsetn0 10085  elcnfn 10089  ellnfn 10090  eigvalval 10103  nmoplb 10111  nmfnlb 10128  eleigvec 10161  0cnop 10182  0cnfn 10183  idcnop 10184  nmlnop0iALT 10199  lnophm 10223  lnopconi 10242  nmbdfnlb 10258  lnfnconi 10269  branmfn 10317  branmfnOLD 10318  bra11 10321  leopg 10335  leoptri 10349  leoptr 10350  hmopidmch 10361  hmopidmpj 10362  elpjrnch 10399  stel 10422  hstel 10423  hstel2 10427  jpi 10478  cvbr 10490  cvcon3 10492  cvnbtwn 10494  mdbr 10502  dmdbr 10507  mdsl1i 10529  mdslmd1lem3 10535  mdslmd1lem4 10536  csmdsymi 10542  elat2 10548  chrelati 10572  chrelat2i 10573  cvexchlem 10576  irred 10604  atcvat4i 10606  mdsymlem2 10613  mdsymlem8 10619  mddmdin0i 10640  cdj1i 10642  cdj3i 10650  elghomlem1 10667  elghomlem2 10668  abfi 10737  ficli 10756  vxveqv 10761  letri31 10791  ac5g 10802  ac6sg 10803  islatalg 10831  cur1val 10846  inposet 10868  isexid 10893  isexid2 10901  exidu1 10902  idrval 10904  cmpidelt 10906  issmgrp 10911  isppm 10917  unmnd 10951  ununr 10955  isdivrng 10968  vri 10981  osneisi 11018  hmeogrp 11044  qusp 11068  isfil 11071  cnfilca 11088  rcfpfillem3 11091  bwt2 11123  clindistop 11131  topsinind 11136  altretoplem2 11143  altretop 11144  trnij 11160  cnvtr 11161  ismgra 11164  isalg 11175  algi 11181  isded 11190  dedi 11191  idosd 11198  iscat 11208  cati 11209  cmpasso 11227  ishomd 11245  ismona 11264  ismonb 11265  imonclem 11268  isepia 11274  isepib 11275  iepiclem 11278  cinvlem1 11282  cinvlem2 11283  cinvlem3 11284  isfuna 11288  isfunb 11289  issubcat 11299  issubcata 11300  issubcatb 11301  infemb 11313  trer 11409  finminlem 11418  elfiun 11421  fictb 11423  ordiso 11426  ordtypelem1 11427  ordtypelem6 11432  ordtype 11434  hartog 11436  opncldf1 11454  opncldf2 11455  opncldf3 11456  cnpnei 11472  subcld 11480  compsublem 11487  compsub 11488  hscptsscld 11491  compfipin0 11493  alexsublem1 11496  alexsublem2 11497  alexsublem3 11498  alexsublem4 11499  connsub 11502  cnconn 11503  subtopmetlem 11505  subtopmet 11506  reconnlem1 11507  2ndcsb 11537  2ndc1stc 11538  2ndcctbss 11539  isfne 11541  isfne3 11543  isref 11549  fness 11552  fneref 11554  fnessref 11564  refssfne 11565  comppfsc 11578  neibastop1 11579  neibastop2lem1 11580  neibastop2lem2 11581  neibastop2lem3 11582  neibastop2lem4 11583  neibastop2 11584  neibastop3 11585  topmtcl 11586  topmeet 11587  topjoin 11588  fnemeet1 11589  fnemeet2 11590  fnejoin1 11591  ist1-2 11603  ist1-3 11604  elfg 11633  fgfil 11638  neifg 11644  supfil 11645  filfinnfr 11646  isufil2 11650  ufilmax 11653  filssufillem 11655  filssufil 11656  ufileu 11658  fixufil 11661  ufinffr 11663  ufilen 11664  filcon 11665  limfilcf 11683  hausfillim 11685  cnpfillim 11686  filmapf 11688  isfilmap 11689  elfilmap 11690  rnelfm 11699  flimff 11707  sflimf 11708  sfcls 11716  fcluscf 11724  flimfnfcls 11727  fcluscnplem 11729  fcluscnp 11730  fclusff 11735  sfclusf 11736  isdir 11749  dirtr 11753  dirge 11754  tosdir 11755  tailf 11756  istail 11757  tailuni 11761  tailfb 11762  filnetlem1 11763  filnetlem2 11764  filnetlem3 11765  filnetlem4 11766  filnetlem5 11767  filnet 11768  isgalem 11771  isga 11772  ssga 11777  gapmlem 11783  gapm 11784  inpreima 11793  opabex3 11806  oprabopabf 11807  upixp 11823  fimaxg 11838  acdcg 11842  acdc3g 11843  acdc5g 11844  indexd 11846  inficl 11849  sdclem2 11876  sdc 11877  fsumltisumi 11886  fsumltisum 11887  iserzshft2 11892  fsumlt1 11894  fiinbas 11905  metsstop 11909  blhalf 11911  mettrifi 11912  caures 11917  metdcn 11918  iccss2 11921  icoopnst 11940  iocopnst 11941  cncfco 11948  haustlmu 11967  uptx 11978  txcnopab 11980  txcnoprab 11981  istotbnd 11989  sstotbnd 11992  totbndss 11993  ismtyval 12003  isismty 12004  ismtyhmeolem 12006  ismtyres 12010  heiborlem1 12011  heiborlem18 12028  heiborlem28 12038  heiborlem30 12040  heiborlem32 12042  heiborlem35 12045  heiborlem36 12046  heiborlem42 12052  bfplem3 12056  bfplem8 12061  bfplem11 12064  bfp 12065  recms 12066  rrnval 12069  rrnmet 12072  rrncms 12075  rrntotbndlem1 12076  rrntotbnd 12078  rrnheibor 12079  reheibor 12081  phtpyfval 12088  phtpyval 12089  isphtpy 12090  phtpycom 12092  phtpyco 12098  phtpcval 12100  isphtpc 12101  phtpcer 12104  ishgrag 12195  hgralem 12196  ispgrag 12205

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 145  df-an 223

Copyright terms: Public domain