Theorem biancomd 466

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 463	. 2 ⊢ ((𝜃 ∧ 𝜒) ↔ (𝜒 ∧ 𝜃))
3	1, 2	syl6bb 289	1 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 399

This theorem is referenced by:  ibar  531  rbaibd  543  pm4.71rd  565  anbi1cd  635  mpbiran2d  706  elpmg  8416  letri3  10720  mulsuble0b  11506  xrletri3  12541  qbtwnre  12586  iooneg  12851  invsym  17026  subsubc  17117  lsslss  19727  znleval  20695  restopn2  21779  elflim2  22566  ismet2  22937  mbfi1fseqlem4  24313  deg1ldg  24680  sincosq1sgn  25078  lgsquadlem3  25952  numclwwlkqhash  28148  rmounid  30253  dfrdg4  33407  bj-19.41t  34098  bj-0int  34387