Theorem bianbi 638

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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anbi12i  639  bianassc  655  pm5.53  1020  dfifp4  1080  dfifp5  1081  an6  1471  an3andi  1510  19.28v  2023  19.28  2270  2eu4  2688  r19.26-3  3132  r19.41v  3201  r3ex  3210  3reeanv  3244  r19.41  3275  rmo4  3702  rmo3f  3706  sbc3an  3817  rmo3  3851  difin2  4262  otelxp  5706  f1ounsn  7271  dfpth2  30019  kardexen  35509  dfrefrel5  39170  dfdisjALTV5a  39376  dfantisymrel4  39437  dfantisymrel5  39438  petseq  39549  redvmptabs  43045  permaxsep  45642  clnbgrel  48516  grimuhgr  48575  catcinv  50096