Theorem bianbi 626

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 623	. 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  627  bianassc  642  pm5.53  1005  dfifp4  1067  dfifp5  1068  an3andi  1482  19.28v  1990  19.28  2229  2eu4  2658  r19.26-3  3118  r19.41v  3195  r3ex  3204  3reeanv  3236  r19.41  3269  rmo4  3752  rmo3f  3756  sbc3an  3874  rmo3  3911  difin2  4320  otelxp  5744  dfrefrel5  38473  dfantisymrel4  38717  dfantisymrel5  38718  clnbgrel  47701  grimuhgr  47762