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 ⊢ (𝜑 ↔ (𝜃 ∧ 𝜒))

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

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 401

This theorem is used by:  anbi12i  639  bianassc  655  pm5.53  1022  dfifp4  1082  dfifp5  1083  an6  1474  an3andi  1513  19.28v  2026  19.28  2264  2eu4  2682  r19.26-3  3126  r19.41v  3195  r3ex  3204  3reeanv  3238  r19.41  3269  rmo4  3693  rmo3f  3697  sbc3an  3808  rmo3  3842  difin2  4254  otelxp  5705  f1ounsn  7270  dfpth2  30087  kardexen  35584  dfrefrel5  39274  dfdisjALTV5a  39480  dfantisymrel4  39541  dfantisymrel5  39542  petseq  39653  redvmptabs  43149  permaxsep  45744  clnbgrel  48621  grimuhgr  48680  catcinv  50205