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  1997  19.28  2233  2eu4  2653  r19.26-3  3095  r19.41v  3164  r3ex  3173  3reeanv  3207  r19.41  3238  rmo4  3686  rmo3f  3690  sbc3an  3803  rmo3  3837  difin2  4251  otelxp  5666  f1ounsn  7216  dfpth2  29751  dfrefrel5  38709  dfantisymrel4  38959  dfantisymrel5  38960  redvmptabs  42557  permaxsep  45190  clnbgrel  48016  grimuhgr  48075  catcinv  49586