Theorem anbi12d 639

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

Syntax hints:   -> wi 3   <-> wb 153   /\ wa 230

This theorem is referenced by:  pm4.38 642  3anbi123d 905  drsb1 1217  sb7f 1383  mopick 1475  clelab 1628  cbvrexf 1844  cbvrex 1846  cbvreuv 1849  gencbvex 1885  rcla4e 1919  eqvincf 1931  ceqsrexv 1936  elrabf 1951  cbvrab 1957  reu2 1977  reu3 1978  rmo4 1980  reu8 1983  cbvsbcv 2007  sbcang 2021  sbcabel 2046  sbcel12g 2062  eldif 2108  psseq1 2186  psseq2 2187  ssconb 2221  elin 2258  elunii 2562  eluniab 2567  cbvopab 2727  cbvopab1 2729  cbvopab1s 2730  cbvopab2v 2732  nalset 2767  elssabg 2781  intabs 2788  unipw 2812  nnullss 2824  exss 2825  opabid 2866  opelopab2 2875  dfid3 2892  poeq1 2898  pocl 2900  soeq1 2909  axun 2923  snnex 2933  fri 2975  frc 2977  weeq1 2994  weeq2 2995  ordeq 3012  onminex 3077  elom 3191  elomg 3192  vtoclr 3268  opbrop 3295  relop 3332  asymref2 3497  elxp4 3510  elxp5 3511  funopg 3604  fununi 3620  funcnvuni 3621  fneq1 3639  2elresin 3655  feq1 3677  fcoi2 3703  f1eq1 3717  foeq1 3725  f1oeq1 3741  f1oeq2 3742  f1oeq3 3743  ffoss 3768  fv3 3790  tz6.12f 3795  fnopabfv 3815  ssimaex 3825  fvopab3 3834  fvopab3ig 3835  fvopab4gf 3838  elunirnALT 3926  isoeq1 3945  isoeq4 3948  isomin 3957  isoini 3958  isofrlem 3959  isowe 3961  f1oweALT 3964  tfrlem1 3969  tfrlem3 3971  tfrlem5 3973  tfrlem12 3980  tz7.44-2 3987  tz7.44-3 3988  rdglem2 3996  cbvoprab12 4056  oprabval 4081  oprabvalig 4082  oprabval2gf 4084  oprabval4g 4089  caoprmo 4128  2ndconst 4155  unielxp 4165  dfoprab5 4173  ertr 4332  ecelqsi 4352  brecop 4367  ecopoprtrn 4372  th3qlem1 4375  th3qlem2 4376  th3q 4378  elpm 4397  elixp2 4410  ixpeq1 4414  mapsnen 4490  fiprOLD 4496  xpsnen 4498  endisj 4500  pw2en 4509  sbthlem2 4511  sbth 4520  php2 4579  nnsdomo 4586  unfilem1 4611  unifi 4618  fiint 4620  abfii4 4624  supeq1 4635  supmo 4636  supub 4640  suplub 4641  supmaxlem 4648  suppr 4650  supsnALT 4652  en2lp 4664  inf0 4668  axinf2 4686  dfom3 4692  unbnn3 4701  rankr1g 4737  r1pwcl 4749  karden 4788  aceq1 4791  aceq0 4792  aceq2 4793  aceq3lem 4794  aceq3 4795  aceq4 4796  aceq5lem1 4797  aceq5lem2 4798  aceq5lem3 4799  aceq5lem4 4800  aceq5 4802  aceq6a 4803  aceq6b 4804  axac 4807  ac7g 4811  ac5 4814  ac6lem 4816  kmlem1 4827  kmlem2 4828  kmlem4 4830  kmlem14 4840  zorn2lem1 4850  zorn2lem7 4856  zorn2 4858  brdom3 4863  brdom7disj 4866  brdom6disj 4867  unidom 4870  cardsdom 4901  alephnbtwn2 4934  aleph11 4944  dominf 4969  cflem 4970  cfval 4971  cflecard 4977  cfeq0 4979  cfsuc 4980  axrepndlem2 5010  axunnd 5013  axregndlem2 5020  axinfndlem1 5022  axacndlem5 5028  axacnd 5029  zfcndun 5032  zfcndac 5036  ltsopi 5081  indpi 5099  ltsopq 5140  ltbtwnpq 5149  elnp 5157  prcdpq 5162  genpv 5167  genpprecl 5169  genpnmax 5175  ltprord 5199  ltsopr 5201  ltexprlem4 5210  ltexprlem7 5213  prlem936 5220  reclem1pr 5221  reclem3pr 5223  supexpr 5228  ltsosr 5268  negexsr 5276  recexsr 5281  suppsr 5287  suppsr3 5289  supsrlem5 5294  supsrlem6 5295  ltresr 5323  supre 5325  ltsor 5326  axrnegex 5348  axrrecex 5349  axcnre 5351  ltxr 5560  axlttrn 5569  axsup 5572  letri3 5582  ltleadd 5710  lesub0 5743  div11 5822  recrec 5834  prodgt0 5884  prodge0 5886  posexi 5968  peano5nni 5986  dfnn2 5996  nn2ge 6002  nominpos 6104  lbinfm 6130  sup2 6133  infm3 6136  dfinfmr 6149  infmsup 6150  nnunb 6152  xrsupsslem 6158  xrinfmsslem 6159  xrsupss 6160  xrinfmss 6161  supxr 6163  zltp1le 6263  z2ge 6273  dfuzi 6287  peano5uzi 6288  uzind 6290  uzindOLD 6293  zmax 6305  rebtwnz 6307  qbtwnre 6331  qbtwnxr 6332  flval 6336  fllelt 6339  flval2 6350  flbi 6352  flbi2 6353  iooin 6397  elioo1 6403  elioo2 6404  elioc1 6406  elico1 6407  elicc1 6408  iooshf 6421  iooneg 6432  iccneg 6433  icoshf 6434  icoshftf1olem 6436  icounlem 6438  icoun 6439  nnwof 6485  elfz1 6496  fzrev 6537  sqr0 6762  sqrlem4 6766  sqrlem24 6786  sqrgt0ii 6787  sqrlem26 6788  sqr2irrlem2 6815  abslt 6970  absle 6971  absdiflt 6973  absdifle 6974  abs1mi 6994  abs3lem 6997  cau3iri 7005  cau5ii 7007  bcval 7048  clim 7067  dffsum 7088  climuni 7189  climshfti 7194  climresi 7195  iserzshft2i 7197  climrecl 7200  climge0 7202  caucvg3 7258  cvgcmp3cetlem1 7278  cvgcmp3cetlem2 7279  iserzgt0 7301  expcnvlem5 7321  geolim 7327  geolim1 7329  fsum0diag 7348  cncfval 7354  elcncf 7355  efseq1ex 7396  absef01tlubi 7478  efcnlem4 7513  reeff1olem2 7516  acdc3 7579  acdc2 7582  acdc5 7585  acdc 7587  infpnlem2 7599  infpn2 7601  ruclem4 7605  ruclem12 7613  ruclem29 7630  ruclem36 7637  infxpidmlem2 7645  infxpidmlem3 7646  infxpidmlem8 7651  infpss 7666  infmap2lem1 7671  istopg 7688  eltopsp 7695  tpsex 7696  istps 7697  eltg2 7708  tgval3 7714  topbas 7716  subtop 7733  cctop 7737  retopbas 7740  cldval 7751  ntrfval 7752  clsfval 7753  iscld 7754  elcls 7789  neifval 7799  isnei 7803  neiint 7804  neips 7812  opnneissb 7813  opnssneib 7814  innei 7821  lpfval 7827  islp2 7832  qdensere 7836  cnpfval 7842  ismet 7883  dfms2 7884  ismsg 7885  msflem 7888  metreslem 7907  blfval 7920  blelrn 7933  blin 7937  blss 7938  blssex 7939  opnfval 7942  opnm 7945  blssopn 7952  opnin 7954  neibl 7962  blnei 7964  metcnp 7972  metcn 7974  metcnpi3 7977  metcnpi4 7978  metcni2 7980  tgioolem 7999  caufval 8011  lmbr 8013  iscau3 8023  iscau4 8025  lmss 8038  lmfex 8044  lmle 8045  metelcls 8050  metcnp4 8055  xpcn 8061  fsumcnlem 8074  iscms2lem4 8077  lmcau 8081  bcthlem2 8085  bcthlem7 8090  bcthlem15 8098  bcth 8117  isgrp 8126  isgrpi 8127  grpideu 8138  grpidinv2 8144  grpinvfval 8150  grpinv 8153  grpdivfval 8165  isring 8225  ringi 8226  ringid 8229  cnring 8246  ringsn 8247  vci 8251  isvclem 8280  nmcnilem 8421  va1cnlem 8429  sm1cnilem 8431  ipfval 8436  lnoval 8497  islno 8498  nmofval 8509  nmosetn0 8512  nmolb 8518  nmlno0lem 8537  blocni 8549  ajmoi 8603  pslem 8731  spwval2 8737  spwmo 8740  spwpr2 8742  spwpr4OLD 8746  spwpr4aOLD 8747  pilem2 8755  pilem3 8756  pilem4 8757  sinperlem2 8770  sincosq1sgn 8787  sincosq2sgn 8788  sincosq3sgn 8789  sincosq4sgn 8790  efifolem2 8806  efifolem3 8807  efifolem6 8810  effoi 8828  normlem7tALT 9068  norm3lemt 9102  hcau 9134  hcau2 9138  hlimi 9139  hlim2 9143  sh 9161  closedsub 9176  chlimi 9187  hlimunii 9192  ch2 9197  hhsssh 9222  ocsh 9239  ocin 9252  projlem7 9275  projlem17 9285  projlem26 9294  projlem28 9296  pjtheu 9319  pjmval 9321  omlsi 9329  pjoml 9352  shintcl 9377  chintcl 9379  shlub 9437  chpsscon3 9509  cmbr 9610  pjoml6i 9615  cm2j 9646  spansncv 9681  pjrni 9730  adjmo 9841  eigre 9844  eigorth 9847  elcnop 9866  ellnop 9867  nmopsetn0 9875  elunop 9882  elhmop 9883  nmfnsetn0 9888  elcnfn 9892  ellnfn 9893  eigvalval 9906  nmoplb 9914  nmfnlb 9931  eleigvec 9964  0cnop 9986  0cnfn 9987  idcnop 9988  nmlnop0iALT 10003  lnophm 10027  lnopconi 10046  nmbdfnlb 10062  lnfnconi 10073  branmfn 10121  bra11 10124  leopg 10138  leoptri 10152  leoptr 10153  hmopidmch 10164  hmopidmpj 10165  elpjrnch 10202  stel 10225  hstel 10226  hstel2 10230  jpi 10281  cvbr 10293  cvcon3 10295  cvnbtwn 10297  mdbr 10305  dmdbr 10310  mdsl1i 10332  mdslmd1lem3 10338  mdslmd1lem4 10339  csmdsymi 10345  elat2 10351  chrelati 10375  chrelat2i 10376  cvexchlem 10379  irred 10406  atcvat4i 10408  mdsymlem2 10415  mdsymlem8 10421  mddmdin0i 10442  cdj1i 10444  cdj3i 10452  elghomlem1 10467  elghomlem2 10468  abfi 10534  ficli 10553  vxveqv 10558  inposet 10578  vri 10583  iseuctopg 10596  hmeogrp 10632  qusp 10649  isfil 10652  cnfilca 10670  rcfpfillem3 10673  sfvlimOLD 10685  trnij 10719  cnvtr 10720  ismgra 10724  isalg 10735  algi 10742  isded 10751  dedi 10752  idosd 10759  iscat 10769  cati 10770  cmpasso 10788  ishomd 10800  ismona 10819  ismonb 10820  imonclem 10823  isepia 10829  isepib 10830  iepiclem 10833  isfuna 10838  isfunb 10839  ishgrag 10853  hgralem 10854  ispgrag 10863

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 154  df-an 232

Copyright terms: Public domain