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  2029  19.28  2267  2eu4  2684  r19.26-3  3128  r19.41v  3197  r3ex  3206  3reeanv  3240  r19.41  3271  rmo4  3695  rmo3f  3699  sbc3an  3810  rmo3  3843  difin2  4254  otelxp  5707  f1ounsn  7279  dfpth2  30145  kardexen  35637  dfrefrel5  39308  dfdisjALTV5a  39514  dfantisymrel4  39575  dfantisymrel5  39576  petseq  39687  redvmptabs  43198  permaxsep  45793  clnbgrel  48670  grimuhgr  48729  catcinv  50253