Theorem biancomd 464

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 461	. 2 ⊢ ((𝜃 ∧ 𝜒) ↔ (𝜒 ∧ 𝜃))
3	1, 2	bitrdi 288	1 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ibar  533  rbaibd  545  pm4.71rd  567  anbi1cd  641  mpbiran2d  714  naddcom  8608  naddsuc2  8627  elpmg  8780  letri3  11222  mulsuble0b  12019  xrletri3  13096  qbtwnre  13142  iooneg  13415  invsym  17720  subsubc  17811  lsslss  20951  znleval  21529  psdmvr  22157  restopn2  23160  elflim2  23947  ismet2  24316  mbfi1fseqlem4  25703  deg1ldg  26075  sincosq1sgn  26480  lgsquadlem3  27363  renegscl  28508  numclwwlkqhash  30463  rmounid  32582  dfrdg4  36179  bj-19.41t  37109  bj-0int  37459  orddif0suc  43713  dflim7  43718  mpbiran4d  49288