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  8674  naddsuc2  8693  elpmg  8845  letri3  11322  mulsuble0b  12114  xrletri3  13208  qbtwnre  13254  iooneg  13527  invsym  17854  subsubc  17945  lsslss  21148  znleval  21770  psdmvr  22400  restopn2  23405  elflim2  24193  ismet2  24562  mbfi1fseqlem4  25949  deg1ldg  26320  sincosq1sgn  26739  lgsquadlem3  27621  renegscl  28766  numclwwlkqhash  30858  rmounid  32973  dfrdg4  36533  bj-19.41t  37502  bj-0int  37854  orddif0suc  44112  dflim7  44117  mpbiran4d  49729