Theorem bianbi 636

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 633	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜃 ∧ 𝜒))
4	1, 3	bitri 277	1 ⊢ (𝜑 ↔ (𝜃 ∧ 𝜒))

Syntax hints:   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  anbi12i  637  bianassc  653  pm5.53  1018  dfifp4  1078  dfifp5  1079  an6  1468  an3andi  1505  19.28v  2018  19.28  2265  2eu4  2683  r19.26-3  3125  r19.41v  3194  r3ex  3203  3reeanv  3237  r19.41  3268  rmo4  3695  rmo3f  3699  sbc3an  3810  rmo3  3844  difin2  4255  otelxp  5693  f1ounsn  7258  dfpth2  29931  dfrefrel5  39101  dfdisjALTV5a  39307  dfantisymrel4  39368  dfantisymrel5  39369  petseq  39480  redvmptabs  42974  permaxsep  45588  clnbgrel  48455  grimuhgr  48514  catcinv  50025