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  635  mpbiran2d  708  naddcom  8600  naddsuc2  8619  elpmg  8770  letri3  11201  mulsuble0b  11997  xrletri3  13056  qbtwnre  13101  iooneg  13374  invsym  17669  subsubc  17760  lsslss  20864  znleval  21461  psdmvr  22054  restopn2  23062  elflim2  23849  ismet2  24219  mbfi1fseqlem4  25617  deg1ldg  25995  sincosq1sgn  26405  lgsquadlem3  27291  renegscl  28367  numclwwlkqhash  30319  rmounid  32439  dfrdg4  35935  bj-19.41t  36758  bj-0int  37085  orddif0suc  43251  dflim7  43256  mpbiran4d  48792