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  2264  2eu4  2679  r19.26-3  3123  r19.41v  3192  r3ex  3201  3reeanv  3235  r19.41  3266  rmo4  3688  rmo3f  3692  sbc3an  3803  rmo3  3836  difin2  4247  otelxp  5699  f1ounsn  7275  dfring3  20454  dfpth2  30222  kardexen  35719  dfrefrel5  39359  dfdisjALTV5a  39565  dfantisymrel4  39626  dfantisymrel5  39627  petseq  39738  redvmptabs  43249  permaxsep  45844  clnbgrel  48758  grimuhgr  48817  catcinv  50339