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  1447  an3andi  1484  19.28v  1996  19.28  2229  2eu4  2648  r19.26-3  3090  r19.41v  3159  r3ex  3168  3reeanv  3202  r19.41  3233  rmo4  3690  rmo3f  3694  sbc3an  3807  rmo3  3841  difin2  4252  otelxp  5663  f1ounsn  7209  dfpth2  29674  dfrefrel5  38504  dfantisymrel4  38749  dfantisymrel5  38750  redvmptabs  42343  permaxsep  44991  clnbgrel  47822  grimuhgr  47881  catcinv  49394