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  8623  naddsuc2  8642  elpmg  8793  letri3  11235  mulsuble0b  12031  xrletri3  13090  qbtwnre  13135  iooneg  13408  invsym  17704  subsubc  17795  lsslss  20899  znleval  21496  psdmvr  22089  restopn2  23097  elflim2  23884  ismet2  24254  mbfi1fseqlem4  25652  deg1ldg  26030  sincosq1sgn  26440  lgsquadlem3  27326  renegscl  28402  numclwwlkqhash  30354  rmounid  32474  dfrdg4  35932  bj-19.41t  36755  bj-0int  37082  orddif0suc  43250  dflim7  43255  mpbiran4d  48779