Theorem biancomd 463

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ibar  528  rbaibd  540  pm4.71rd  562  anbi1cd  636  mpbiran2d  709  naddcom  8620  naddsuc2  8639  elpmg  8792  letri3  11230  mulsuble0b  12026  xrletri3  13080  qbtwnre  13126  iooneg  13399  invsym  17698  subsubc  17789  lsslss  20927  znleval  21524  psdmvr  22127  restopn2  23136  elflim2  23923  ismet2  24292  mbfi1fseqlem4  25690  deg1ldg  26068  sincosq1sgn  26478  lgsquadlem3  27364  renegscl  28509  numclwwlkqhash  30466  rmounid  32585  dfrdg4  36171  bj-19.41t  37013  bj-0int  37358  orddif0suc  43629  dflim7  43634  mpbiran4d  49161