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  8424  letri3  10728  mulsuble0b  11514  xrletri3  12550  qbtwnre  12595  iooneg  12860  invsym  17034  subsubc  17125  lsslss  19735  znleval  20703  restopn2  21787  elflim2  22574  ismet2  22945  mbfi1fseqlem4  24321  deg1ldg  24688  sincosq1sgn  25086  lgsquadlem3  25960  numclwwlkqhash  28156  rmounid  30261  dfrdg4  33414  bj-19.41t  34105  bj-0int  34395