Theorem biancomd 462

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  ibar  527  rbaibd  539  pm4.71rd  561  anbi1cd  633  mpbiran2d  706  naddcom  8701  elpmg  8860  letri3  11329  mulsuble0b  12116  xrletri3  13165  qbtwnre  13210  iooneg  13480  invsym  17744  subsubc  17838  lsslss  20849  znleval  21492  restopn2  23111  elflim2  23898  ismet2  24269  mbfi1fseqlem4  25678  deg1ldg  26058  sincosq1sgn  26463  lgsquadlem3  27345  renegscl  28282  numclwwlkqhash  30241  rmounid  32350  dfrdg4  35617  bj-19.41t  36321  bj-0int  36650  orddif0suc  42762  dflim7  42767  naddsuc2  42887  mpbiran4d  47982