Theorem biancomd 469

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ibar  538  rbaibd  550  pm4.71rd  572  anbi1cd  647  mpbiran2d  721  naddcom  8675  naddsuc2  8694  elpmg  8846  letri3  11312  mulsuble0b  12104  xrletri3  13197  qbtwnre  13243  iooneg  13516  invsym  17843  subsubc  17934  lsslss  21134  znleval  21756  psdmvr  22384  restopn2  23386  elflim2  24174  ismet2  24543  mbfi1fseqlem4  25930  deg1ldg  26302  sincosq1sgn  26716  lgsquadlem3  27599  renegscl  28744  numclwwlkqhash  30799  rmounid  32914  dfrdg4  36482  bj-19.41t  37450  bj-0int  37802  orddif0suc  44055  dflim7  44060  mpbiran4d  49635