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  8597  naddsuc2  8616  elpmg  8767  letri3  11198  mulsuble0b  11994  xrletri3  13053  qbtwnre  13098  iooneg  13371  invsym  17669  subsubc  17760  lsslss  20894  znleval  21491  psdmvr  22084  restopn2  23092  elflim2  23879  ismet2  24248  mbfi1fseqlem4  25646  deg1ldg  26024  sincosq1sgn  26434  lgsquadlem3  27320  renegscl  28400  numclwwlkqhash  30355  rmounid  32474  dfrdg4  35995  bj-19.41t  36818  bj-0int  37145  orddif0suc  43371  dflim7  43376  mpbiran4d  48908