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  2265  2eu4  2680  r19.26-3  3124  r19.41v  3193  r3ex  3202  3reeanv  3236  r19.41  3267  rmo4  3688  rmo3f  3692  sbc3an  3803  rmo3  3836  difin2  4247  otelxp  5695  f1ounsn  7280  dfring3  20518  lgsquadlem1  27707  dfpth2  30314  kardexen  35831  dfrefrel5  39529  dfdisjALTV5a  39735  dfantisymrel4  39796  dfantisymrel5  39797  petseq  39908  redvmptabs  43411  permaxsep  45996  clnbgrel  48925  grimuhgr  48984  catcinv  50506