Theorem anbi12i 369

Description: Conjoin both sides of two equivalences.

Hypotheses

Ref	Expression
bi2an.1	⊢ (φ ↔ ψ)
bi2an.2	⊢ (χ ↔ θ)

Assertion

Ref	Expression
anbi12i	⊢ ((φ ∧ χ) ↔ (ψ ∧ θ))

Proof of Theorem anbi12i

Step	Hyp	Ref	Expression
1		bi2an.1	. . 3 ⊢ (φ ↔ ψ)
2	1	anbi1i 368	. 2 ⊢ ((φ ∧ χ) ↔ (ψ ∧ χ))
3		bi2an.2	. . 3 ⊢ (χ ↔ θ)
4	3	anbi2i 367	. 2 ⊢ ((ψ ∧ χ) ↔ (ψ ∧ θ))
5	2, 4	bitr 151	1 ⊢ ((φ ∧ χ) ↔ (ψ ∧ θ))

Syntax hints:   ↔ wb 127   ∧ wa 196

This theorem is referenced by:  pm4.11 400  bicon2 403  ordir 453  jcab 454  andi 456  orddi 458  dfbi 499  rnlem 579  bi3an 606  an6 638  19.43 767  sbbi 890  eu1 1019  euanv 1053  2exeu 1066  2eu1 1067  2eu4 1070  r19.26 1289  r19.26m 1291  r19.29 1295  reeanv 1316  reu2 1338  eqss 1516  pssn2lp 1571  reuss 1577  reupick 1578  unss 1632  ssin 1659  undi 1677  inab 1692  prsspw 1858  ssext 1865  pweqb 1867  pwin 1915  uniin 1935  intun 1989  intpr 1990  efrn2lp 2181  wetrep 2194  onminex 2275  sucelon 2319  opelxp 2452  elxp3 2460  weinxp 2467  relun 2490  inopab 2495  inxp 2496  opelcog 2511  cnvco 2520  dmin 2537  dfima2 2604  intasym 2627  cnvin 2643  relssdr 2668  dmco2 2673  dffun4 2676  funun 2700  fununi 2705  imadif 2714  fun 2763  fint 2769  fin 2770  f1cnv 2782  f1co 2783  f1o3 2805  f1oco 2816  tz6.12 2843  fsn 2895  isotr 2935  isotrALT 2936  tfrlem5 2953  tfrlem7 2955  elxp6 3093  er2 3201  ider 3208  brecop 3242  th3qlem1 3250  oprec 3254  brsdom 3286  map1 3335  xpcomen 3343  xpassen 3344  sbthlem9 3357  sbthlem10 3358  sbthcl 3361  brsdom2 3363  mapenlem2 3385  xpmapenlem5 3395  mapunen 3397  ssenen 3399  inf4 3473  zfinf 3474  scottexs 3543  scott0s 3544  kardex 3550  karden 3551  aceq5lem1 3558  aceq5lem3 3560  kmlem15 3594  genpass 3906  addcompr 3917  mulcompr 3919  distrlem3pr 3923  mulgt0sr 4008  elreal 4044  addcnsr 4047  mulcnsr 4048  ltresr 4052  ltsor 4055  axaddex 4059  axmulex 4060  axcnre 4087  muln0bt 4213  creur 4532  creui 4533  nnwos 4610  zmin 4617  abs00 4839  ruclem15 4899  infxpidmlem7 4939  shscl 5282  sshjvalt 5321  sshjval3t 5327  chcon2 5386  chcon3 5387  spanun 5450  hosmvalt 5487  hodmvalt 5488  5oalem7 5550  3oalem3 5554  pjin2 5647  pjin3 5648  cvnbtwn4t 5721

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org