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  3690  rmo3f  3694  sbc3an  3807  rmo3  3841  difin2  4255  otelxp  5678  f1ounsn  7230  dfpth2  29820  dfrefrel5  38877  dfdisjALTV5a  39083  dfantisymrel4  39144  dfantisymrel5  39145  petseq  39256  redvmptabs  42759  permaxsep  45392  clnbgrel  48217  grimuhgr  48276  catcinv  49787