Theorem biancomd 469

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 466	. 2 ⊢ ((𝜃 ∧ 𝜒) ↔ (𝜒 ∧ 𝜃))
3	1, 2	bitrdi 290	1 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ibar  538  rbaibd  550  pm4.71rd  572  anbi1cd  647  mpbiran2d  721  naddcom  8703  naddsuc2  8722  elpmg  8874  letri3  11405  mulsuble0b  12199  xrletri3  13293  qbtwnre  13339  iooneg  13612  invsym  17949  subsubc  18040  lsslss  21248  znleval  21872  psdmvr  22502  restopn2  23507  elflim2  24295  ismet2  24664  mbfi1fseqlem4  26051  deg1ldg  26422  sincosq1sgn  26839  lgsquadlem3  27721  renegscl  28896  numclwwlkqhash  30988  rmounid  33145  dfrdg4  36842  bj-19.41t  37795  bj-0int  38161  orddif0suc  44410  dflim7  44415  mpbiran4d  50047