Theorem bianbi 628

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 625	. 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  629  bianassc  644  pm5.53  1007  dfifp4  1067  dfifp5  1068  an6  1448  an3andi  1485  19.28v  1998  19.28  2236  2eu4  2655  r19.26-3  3098  r19.41v  3167  r3ex  3176  3reeanv  3210  r19.41  3241  rmo4  3676  rmo3f  3680  sbc3an  3793  rmo3  3827  difin2  4241  otelxp  5675  f1ounsn  7227  dfpth2  29797  dfrefrel5  38918  dfdisjALTV5a  39124  dfantisymrel4  39185  dfantisymrel5  39186  petseq  39297  redvmptabs  42792  permaxsep  45434  clnbgrel  48304  grimuhgr  48363  catcinv  49874