Theorem anbi12i 482

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 481	. 2 |- ((ph /\ ch) <-> (ps /\ ch))
3		anbi12.2	. . 3 |- (ch <-> th)
4	3	anbi2i 480	. 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 522  con2bi 525  ordir 597  jcab 598  andi 604  orddi 606  pm5.17 668  dfbi3 670  rnlem 773  3anbi123i 822  an6 902  19.43 1088  sbbi 1239  eu1 1392  euan 1428  2exeu 1446  2eu1 1449  2eu4 1452  2eu6 1454  sbabel 1584  neanior 1639  r19.26 1750  r19.26m 1752  r19.29 1756  reeanv 1778  reu2 1930  reu6 1932  eqss 2077  pssn2lp 2147  unss 2204  ssin 2232  undi 2252  inab 2268  reuss2 2275  reupick 2279  ralpr 2428  rexpr 2429  difprsn 2465  prsspw 2480  uniin 2520  intun 2562  intpr 2563  ssext 2763  pweqb 2765  pwin 2825  pwundif 2828  efrn2lp 2929  wetrep 2942  onminex 3020  sucelon 3068  opelxp 3214  elxp3 3224  weinxp 3233  relun 3261  inopab 3268  inxp 3269  opelcog 3290  cnvco 3300  dmin 3318  dfima2 3405  intasym 3438  asymref 3439  cnvin 3456  xpnz 3466  xp11 3476  relssdr 3513  cnvpo 3522  cnvso 3523  dffun4 3528  funun 3554  fun11 3562  fununi 3563  imadif 3574  fun 3641  fint 3650  fin 3651  f1cnv 3666  f1co 3667  foco 3682  f1o3 3694  f1oco 3707  fsn 3834  f1ofv 3877  isotr 3897  isotrALT 3898  tfrlem5 3915  tfrlem7 3917  elxp6 4102  dfoprab5 4115  foprab2 4119  dfer2 4262  ider 4269  eqer 4271  brecop 4306  th3qlem1 4314  oprec 4318  mapval2 4335  brsdom 4381  map1 4430  xpcomen 4439  xpassen 4441  sbthlem9 4455  sbthlem10 4456  sbthcl 4459  brsdom2 4461  mapenlem2 4490  xpmapenlem5 4500  mapunen 4502  ssenen 4504  unfi 4551  axinf2 4624  zfinf 4626  scottexs 4718  scott0s 4719  kardex 4725  karden 4726  aceq5lem1 4735  aceq5lem3 4737  kmlem15 4779  brdom7disj 4804  genpass 5112  addcompr 5123  mulcompr 5125  distrlem3pr 5129  mulgt0sr 5214  elreal 5250  addcnsr 5253  mulcnsr 5254  ltresr 5258  ltsor 5261  axcnre 5286  1re 5435  infmsup 6068  infmxrcl 6086  zmin 6219  nnwos 6460  elfzuzb 6476  creur 6742  creui 6743  abs00 6842  cvganz 6924  cvganuz 6925  dffsum 6998  climmullem8 7127  isupivth 7290  reef11 7408  ruclem15 7524  infxpidmlem7 7558  tgval2t 7617  fctopOLD 7650  cctop 7652  bopcnlem1 7981  fsumcnlem 7989  bcthlem32 8030  ajfval 8469  spwval2 8653  cosh111lem3 8716  grothprim 8783  shscl 9281  sshjvalt 9320  sshjval3t 9326  chcon2 9387  chcon3 9389  spanun 9467  hosmvalt 9511  hodmvalt 9513  hfsmvalt 9514  5oalem7 9605  3oalem3 9609  adjbdlnt 10016  pjin2 10121  pjin3 10122  cvnbtwn4t 10216  mdslj1 10246  mdslj2 10247  mdslmd1 10256  mdsldmd1 10258  chrelat4 10300  irred 10321  cdj3lem3 10365  cdj3lem3b 10367  cdj3 10368  elghom 10384  symgoprab 10402  symgf 10405  symggrpi 10406

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