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 286	1 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  ibar  528  rbaibd  540  pm4.71rd  562  anbi1cd  633  mpbiran2d  704  elpmg  8589  letri3  10991  mulsuble0b  11777  xrletri3  12817  qbtwnre  12862  iooneg  13132  invsym  17391  subsubc  17484  lsslss  20138  znleval  20674  restopn2  22236  elflim2  23023  ismet2  23394  mbfi1fseqlem4  24788  deg1ldg  25162  sincosq1sgn  25560  lgsquadlem3  26435  numclwwlkqhash  28640  rmounid  30744  naddcom  33762  dfrdg4  34180  bj-19.41t  34883  bj-0int  35199  mpbiran4d  46031