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  8721  naddsuc2  8740  elpmg  8884  letri3  11347  mulsuble0b  12141  xrletri3  13197  qbtwnre  13242  iooneg  13512  invsym  17807  subsubc  17899  lsslss  20960  znleval  21574  psdmvr  22174  restopn2  23186  elflim2  23973  ismet2  24344  mbfi1fseqlem4  25754  deg1ldg  26132  sincosq1sgn  26541  lgsquadlem3  27427  renegscl  28431  numclwwlkqhash  30395  rmounid  32515  dfrdg4  35953  bj-19.41t  36776  bj-0int  37103  orddif0suc  43286  dflim7  43291  mpbiran4d  48723