Theorem bianbi 634

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

Syntax hints:   ↔ wb 208   ∧ wa 397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 398

This theorem is referenced by:  anbi12i  635  bianassc  650  pm5.53  1013  dfifp4  1073  dfifp5  1074  an6  1454  an3andi  1491  19.28v  2004  19.28  2242  2eu4  2660  r19.26-3  3102  r19.41v  3171  r3ex  3180  3reeanv  3214  r19.41  3245  rmo4  3673  rmo3f  3677  sbc3an  3789  rmo3  3823  difin2  4232  otelxp  5665  f1ounsn  7220  dfpth2  29819  dfrefrel5  38979  dfdisjALTV5a  39185  dfantisymrel4  39246  dfantisymrel5  39247  petseq  39358  redvmptabs  42852  permaxsep  45466  clnbgrel  48333  grimuhgr  48392  catcinv  49903