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  an3andi  1481  19.28v  1988  19.28  2226  2eu4  2653  r19.26-3  3110  r19.41v  3187  r3ex  3196  3reeanv  3228  r19.41  3261  rmo4  3739  rmo3f  3743  sbc3an  3861  rmo3  3898  difin2  4307  otelxp  5733  f1ounsn  7292  dfrefrel5  38499  dfantisymrel4  38743  dfantisymrel5  38744  redvmptabs  42369  clnbgrel  47753  grimuhgr  47816