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  2649  r19.26-3  3094  r19.41v  3169  r3ex  3178  3reeanv  3212  r19.41  3243  rmo4  3709  rmo3f  3713  sbc3an  3826  rmo3  3860  difin2  4272  otelxp  5690  f1ounsn  7254  dfpth2  29666  dfrefrel5  38502  dfantisymrel4  38746  dfantisymrel5  38747  redvmptabs  42340  permaxsep  44969  clnbgrel  47784  grimuhgr  47842  catcinv  49291