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  634  mpbiran2d  707  naddcom  8738  naddsuc2  8757  elpmg  8901  letri3  11375  mulsuble0b  12167  xrletri3  13216  qbtwnre  13261  iooneg  13531  invsym  17823  subsubc  17917  lsslss  20982  znleval  21596  restopn2  23206  elflim2  23993  ismet2  24364  mbfi1fseqlem4  25773  deg1ldg  26151  sincosq1sgn  26558  lgsquadlem3  27444  renegscl  28448  numclwwlkqhash  30407  rmounid  32523  dfrdg4  35915  bj-19.41t  36740  bj-0int  37067  orddif0suc  43230  dflim7  43235  mpbiran4d  48531