Theorem anbi1i 368

Description: Introduce a right conjunct to both sides of a logical equivalence.

Hypothesis

Ref	Expression
bi.aa	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
anbi1i	⊢ ((φ ∧ χ) ↔ (ψ ∧ χ))

Proof of Theorem anbi1i

Step	Hyp	Ref	Expression
1		ancom 333	. 2 ⊢ ((φ ∧ χ) ↔ (χ ∧ φ))
2		bi.aa	. . 3 ⊢ (φ ↔ ψ)
3	2	anbi2i 367	. 2 ⊢ ((χ ∧ φ) ↔ (χ ∧ ψ))
4		ancom 333	. 2 ⊢ ((χ ∧ ψ) ↔ (ψ ∧ χ))
5	1, 3, 4	3bitr 155	1 ⊢ ((φ ∧ χ) ↔ (ψ ∧ χ))

Syntax hints:   ↔ wb 127   ∧ wa 196

This theorem is referenced by:  anbi12i 369  an12 370  anandi 392  bibi2i 460  xor 500  biass 511  prlem2 577  3ancoma 588  an6 638  19.28 751  euanv 1053  sbabel 1189  r19.27av 1293  r19.29 1295  r19.41v 1302  rexcom 1313  reu5 1339  gencbvex 1372  zfrep4 1479  inass 1650  dfun2 1668  symdif2 1690  undif4 1744  difin0ss 1753  copsexg 1902  iunxsn 2034  iunxun 2035  opabid 2099  wefrc 2195  onpwsuc 2315  dfom2 2374  opelxp 2452  xpundir 2462  cbvop 2473  dmres 2584  iss 2599  imasn 2616  elimasn 2617  elxp4 2640  elxp5 2641  dminss 2648  imainss 2649  imaiun 2650  cores 2659  coi1 2665  coass 2667  dffun2 2674  funin 2708  imadif 2714  fcoi1 2765  fcoi2 2766  fcnvres 2768  f1o3 2805  f1ores 2813  f1oco 2816  ffoss 2820  f11o 2821  fv2 2828  tz6.12-1 2842  fvopabn 2873  fopabfv 2894  fsn 2895  dfoprab2 3021  fnoprval 3042  foprval 3043  ec2 3203  snec 3232  oprec 3254  map0e 3266  domen 3284  mapsnen 3334  xpsnen 3339  xpcomen 3343  xpassen 3344  sbthlem9 3357  xpmapenlem5 3395  zfregs 3491  cp 3547  bnd2 3549  aceq5lem1 3558  aceq5lem2 3559  aceq5lem5 3562  kmlem3 3582  zfcndrep 3760  ltexpi 3823  1pr 3911  distrlem5pr 3925  ltexprlem4 3939  reclem1pr 3950  reclem2pr 3951  addcnsr 4047  mulcnsr 4048  ltresr 4052  axaddex 4059  axmulex 4060  axrrecex 4081  lesub0 4341  elnnz 4572  elnn0z 4574  sqrval 4729  infxpidmlem7 4939  infxpidmlem9 4941  ocvalt 5161  spanvalt 5300  hsupval2t 5301  sshjvalt 5321  sshjval3t 5327  hosmvalt 5487  hodmvalt 5488  cvnbtwn3t 5720  cvnbtwn4t 5721  sumdmdi 5785

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