Theorem anbi12i 484

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 483	. 2 |- ((ph /\ ch) <-> (ps /\ ch))
3		anbi12.2	. . 3 |- (ch <-> th)
4	3	anbi2i 482	. 2 |- ((ps /\ ch) <-> (ps /\ th))
5	2, 4	bitr 173	1 |- ((ph /\ ch) <-> (ps /\ th))

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

This theorem is referenced by:  pm4.11 524  con2bi 527  ordir 599  jcab 600  andi 606  orddi 608  pm5.17 670  dfbi3 672  rnlem 775  3anbi123i 824  an6 904  19.43 1090  sbbi 1241  eu1 1394  euan 1430  2exeu 1449  2eu1 1452  2eu4 1455  2eu6 1457  sbabel 1587  neanior 1642  r19.26 1753  r19.26m 1755  r19.29 1759  reeanv 1781  reu2 1933  reu6 1935  eqss 2080  pssn2lp 2150  unss 2207  ssin 2235  undi 2255  inab 2271  reuss2 2278  reupick 2282  ralpr 2432  rexpr 2433  difprsn 2469  prsspw 2484  uniin 2524  intun 2566  intpr 2567  ssext 2769  pweqb 2771  pwin 2831  pwundif 2834  efrn2lp 2935  wetrep 2948  onminex 3026  sucelon 3074  opelxp 3220  elxp3 3230  weinxp 3239  relun 3267  inopab 3274  inxp 3275  opelcog 3296  cnvco 3306  dmin 3324  dfima2 3411  intasym 3444  asymref 3445  cnvin 3462  xpnz 3472  xp11 3482  relssdr 3519  cnvpo 3528  cnvso 3529  dffun4 3534  funun 3560  fun11 3568  fununi 3569  imadif 3580  fun 3647  fint 3656  fin 3657  f1cnv 3672  f1co 3673  foco 3688  f1o3 3700  f1oco 3713  fsn 3840  f1ofv 3883  isotr 3903  isotrALT 3904  tfrlem5 3921  tfrlem7 3923  elxp6 4108  dfoprab5 4121  foprab2 4125  dfer2 4268  ider 4275  eqer 4277  brecop 4312  th3qlem1 4320  oprec 4324  mapval2 4341  brsdom 4387  map1 4436  xpcomen 4445  xpassen 4447  sbthlem9 4461  sbthlem10 4462  sbthcl 4465  brsdom2 4467  mapenlem2 4496  xpmapenlem5 4506  mapunen 4508  ssenen 4510  unfi 4563  axinf2 4633  zfinf 4635  scottexs 4728  scott0s 4729  kardex 4735  karden 4736  aceq5lem1 4745  aceq5lem3 4747  kmlem15 4789  brdom7disj 4814  genpass 5124  addcompr 5135  mulcompr 5137  distrlem3pr 5141  mulgt0sr 5226  elreal 5262  addcnsr 5265  mulcnsr 5266  ltresr 5270  ltsor 5273  axcnre 5298  1re 5447  infmsup 6070  infmxrcl 6088  zmin 6221  nnwos 6461  elfzuzb 6477  creur 6743  creui 6744  abs00 6842  cvganz 6924  cvganuz 6925  dffsum 6998  climmullem8 7127  isupivth 7290  reef11 7408  ruclem15 7525  infxpidmlem7 7559  tgval2t 7616  fctopOLD 7647  cctop 7649  bopcnlem1 7978  fsumcnlem 7986  bcthlem32 8027  ajfval 8465  spwval2 8649  cosh111lem3 8711  grothprim 8778  shscl 9276  sshjvalt 9315  sshjval3t 9321  chcon2 9382  chcon3 9384  spanun 9462  hosmvalt 9506  hodmvalt 9508  hfsmvalt 9509  5oalem7 9600  3oalem3 9604  adjbdlnt 10011  pjin2 10116  pjin3 10117  cvnbtwn4t 10211  mdslj1 10241  mdslj2 10242  mdslmd1 10251  mdsldmd1 10253  chrelat4 10295  irred 10316  cdj3lem3 10360  cdj3lem3b 10362  cdj3 10363  elghom 10379  symgoprab 10397  symgf 10400  symggrpi 10401  inposet 10477

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