Theorem anbi12i 485

Description: Conjoin both sides of two equivalences.

Hypotheses

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

Assertion

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

Proof of Theorem anbi12i

Step	Hyp	Ref	Expression
1		anbi12.1	. . 3 |- (ph <-> ps)
2	1	anbi1i 484	. 2 |- ((ph /\ ch) <-> (ps /\ ch))
3		anbi12.2	. . 3 |- (ch <-> th)
4	3	anbi2i 483	. 2 |- ((ps /\ ch) <-> (ps /\ th))
5	2, 4	bitri 171	1 |- ((ph /\ ch) <-> (ps /\ th))

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

This theorem is referenced by:  notbi 525  con2bi 528  ordir 600  jcab 601  andi 607  orddi 609  pm5.17 671  dfbi3 673  rnlem 778  3anbi123i 828  an6 908  nic-justbi 964  nic-axALT 970  19.43 1124  sbbi 1276  eu1 1431  euan 1467  2exeu 1486  2eu1 1489  2eu4 1492  2eu6 1494  sbabel 1627  neanior 1685  r19.26 1796  r19.26m 1798  r19.29 1802  reeanv 1824  reu2 1976  reu6 1978  eqss 2129  pssn2lp 2199  unss 2256  ssin 2284  undi 2304  inab 2320  reuss2 2327  reupick 2331  ralpr 2486  rexpr 2487  difprsn 2529  prsspw 2545  uniin 2587  intun 2629  intpr 2630  ssext 2840  pweqb 2842  pwin 2903  pwundif 2906  efrn2lp 2958  wetrep 2969  onminex 3164  sucelon 3174  opelxp 3297  elxp3 3309  weinxp 3319  relun 3350  inopab 3361  inxp 3362  opelco2g 3380  cnvco 3391  dmin 3409  dfima2 3497  intasym 3530  asymref 3531  cnvin 3541  xpnz 3551  xp11 3561  dfco2 3598  relssdmrn 3617  cnvpo 3627  cnvso 3628  dffun4 3633  funun 3659  fun11 3667  fununi 3668  imadif 3679  fun 3748  fint 3757  fin 3758  f1cnv 3773  f1co 3774  foco 3790  dff1o3 3802  f1oco 3818  fsn 3948  dff1o6 3991  isotr 4011  isotrALT 4012  elxp6 4161  dfoprab3s 4175  dfoprab5sf 4178  foprab2 4181  fparlem3 4201  fparlem4 4202  fsplit 4204  tfrlem5 4216  tfrlem7 4218  dfer2 4402  ider 4409  eqer 4411  brecop 4447  th3qlem1 4455  oprec 4459  mapval2 4476  brsdom 4522  map1 4571  xpcomen 4580  xpassen 4582  sbthlem9 4600  sbthlem10 4601  sbthcl 4604  brsdom2 4606  mapenlem2 4637  xpmapenlem5 4647  mapunen 4649  ssenen 4651  unfi 4697  axinf2 4769  zfinf2 4771  scottexs 4864  scott0s 4865  kardex 4871  karden 4872  aceq5lem1 4881  aceq5lem3 4883  kmlem15 4925  brdom7disj 4950  genpass 5266  addcompr 5277  mulcompr 5279  distrlem3pr 5283  mulgt0sr 5368  elreal 5404  addcnsr 5407  mulcnsr 5408  ltresr 5412  ltsor 5415  axcnre 5440  1re 5589  infmsup 6236  infmxrcl 6254  zmin 6391  nnwos 6587  elfzuzb 6604  creur 6943  creui 6944  abs00i 7044  cvganz 7127  cvganuzi 7128  dffsum 7201  climmullem8 7330  isupivthi 7495  reef11i 7616  ruclem15 7736  infxpidmlem7 7770  tgval2 7829  cctop 7862  bopcnlem1 8192  fsumcnlem 8200  bcthlem32 8241  ajfval 8724  spwval2 8915  cosh111lem3 8988  grothpw 9054  axgroth5 9055  grothprim 9057  shscli 9557  sshjval 9596  sshjval3 9602  chcon2i 9663  chcon3i 9665  spanuni 9743  hosmval 9787  hodmval 9789  hfsmval 9790  5oalem7 9883  3oalem3 9887  adjbdln 10295  pjin2i 10402  pjin3i 10403  cvnbtwn4 10497  mdslj1i 10527  mdslj2i 10528  mdslmd1i 10537  mdsldmd1i 10539  chrelat4i 10581  irredi 10603  cdj3lem3 10647  cdj3lem3b 10649  cdj3i 10650  elghom 10669  symgoprab 10687  symgf 10690  symggrpi 10691  anddi2 10718  int2rel 10770  inposet 10868  definc 10869  isexid 10893  trer 11409  fictb 11423  opncldf1 11454  dfcon2 11501  is1stc3 11530  2ndcctbss 11539  neibastop1 11579  opnfbas 11629  extbas1 11641  filrn 11643  neifg 11644  filssufillem 11655  ufinffr 11663  ufilen 11664  rnelfmlem 11698  fmfnfmlem3 11702  filnetlem3 11765  filnetlem4 11766  gapm 11784  difxp 11798  inixp 11820  fsum00 11883  iimulcl 11938  txbas 11973  txcnoprab 11981  heiborlem20 12030  bfp 12065  phtpycom 12092

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