Theorem bianbi 628

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anbi12i  629  bianassc  644  pm5.53  1007  dfifp4  1067  dfifp5  1068  an6  1448  an3andi  1485  19.28v  1998  19.28  2236  2eu4  2656  r19.26-3  3099  r19.41v  3168  r3ex  3177  3reeanv  3211  r19.41  3242  rmo4  3677  rmo3f  3681  sbc3an  3794  rmo3  3828  difin2  4242  otelxp  5670  f1ounsn  7222  dfpth2  29816  dfrefrel5  38936  dfdisjALTV5a  39142  dfantisymrel4  39203  dfantisymrel5  39204  petseq  39315  redvmptabs  42810  permaxsep  45456  clnbgrel  48320  grimuhgr  48379  catcinv  49890