Theorem biancomd 467

Description: Commuting conjunction in a biconditional, deduction form. (Contributed by Peter Mazsa, 3-Oct-2018.)

Hypothesis

Ref	Expression
biancomd.1	⊢ (𝜑 → (𝜓 ↔ (𝜃 ∧ 𝜒)))

Assertion

Ref	Expression
biancomd	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Proof of Theorem biancomd

Step	Hyp	Ref	Expression
1		biancomd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜃 ∧ 𝜒)))
2		ancom 464	. 2 ⊢ ((𝜃 ∧ 𝜒) ↔ (𝜒 ∧ 𝜃))
3	1, 2	syl6bb 290	1 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  ibar  532  rbaibd  544  pm4.71rd  566  anbi1cd  636  mpbiran2d  707  elpmg  8405  letri3  10715  mulsuble0b  11501  xrletri3  12535  qbtwnre  12580  iooneg  12849  invsym  17024  subsubc  17115  lsslss  19726  znleval  20246  restopn2  21782  elflim2  22569  ismet2  22940  mbfi1fseqlem4  24322  deg1ldg  24693  sincosq1sgn  25091  lgsquadlem3  25966  numclwwlkqhash  28160  rmounid  30266  dfrdg4  33525  bj-19.41t  34218  bj-0int  34516