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  8699  naddsuc2  8718  elpmg  8862  letri3  11325  mulsuble0b  12119  xrletri3  13175  qbtwnre  13220  iooneg  13493  invsym  17780  subsubc  17871  lsslss  20923  znleval  21520  psdmvr  22112  restopn2  23120  elflim2  23907  ismet2  24277  mbfi1fseqlem4  25676  deg1ldg  26054  sincosq1sgn  26464  lgsquadlem3  27350  renegscl  28406  numclwwlkqhash  30361  rmounid  32481  dfrdg4  35974  bj-19.41t  36797  bj-0int  37124  orddif0suc  43267  dflim7  43272  mpbiran4d  48757