Theorem bianbi 639

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anbi12i  640  bianassc  656  pm5.53  1022  dfifp4  1082  dfifp5  1083  an6  1474  an3andi  1513  19.28v  2030  19.28  2267  2eu4  2682  r19.26-3  3127  r19.41v  3196  r3ex  3205  3reeanv  3239  r19.41  3270  rmo4  3691  rmo3f  3695  sbc3an  3806  rmo3  3840  difin2  4249  otelxp  5699  f1ounsn  7290  dfring3  20533  lgsquadlem1  27722  dfpth2  30329  kardexen  35905  dfrefrel5  39675  dfdisjALTV5a  39881  dfantisymrel4  39942  dfantisymrel5  39943  petseq  40054  redvmptabs  43557  permaxsep  46142  clnbgrel  49071  grimuhgr  49130  elixpmpt  50149  catcinv  50679