Theorem bianbi 627

Description: Exchanging conjunction in a biconditional. (Contributed by Peter Mazsa, 31-Jul-2023.)

Hypotheses

Ref	Expression
bianbi.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
bianbi.2	⊢ (𝜓 ↔ 𝜃)

Assertion

Ref	Expression
bianbi	⊢ (𝜑 ↔ (𝜃 ∧ 𝜒))

Proof of Theorem bianbi

Step	Hyp	Ref	Expression
1		bianbi.1	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2		bianbi.2	. . 3 ⊢ (𝜓 ↔ 𝜃)
3	2	anbi1i 624	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜃 ∧ 𝜒))
4	1, 3	bitri 275	1 ⊢ (𝜑 ↔ (𝜃 ∧ 𝜒))

Syntax hints:   ↔ wb 206   ∧ wa 395

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

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  anbi12i  628  bianassc  643  pm5.53  1006  dfifp4  1066  dfifp5  1067  an6  1446  an3andi  1483  19.28v  1989  19.28  2227  2eu4  2653  r19.26-3  3099  r19.41v  3176  r3ex  3185  3reeanv  3217  r19.41  3250  rmo4  3720  rmo3f  3724  sbc3an  3837  rmo3  3871  difin2  4283  otelxp  5711  f1ounsn  7275  dfpth2  29696  dfrefrel5  38459  dfantisymrel4  38703  dfantisymrel5  38704  redvmptabs  42335  clnbgrel  47761  grimuhgr  47824