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  8692  naddsuc2  8711  elpmg  8863  letri3  11395  mulsuble0b  12189  xrletri3  13283  qbtwnre  13329  iooneg  13602  invsym  17937  subsubc  18028  lsslss  21236  znleval  21860  psdmvr  22490  restopn2  23495  elflim2  24283  ismet2  24652  mbfi1fseqlem4  26039  deg1ldg  26410  sincosq1sgn  26827  lgsquadlem3  27709  renegscl  28884  numclwwlkqhash  30976  rmounid  33091  dfrdg4  36715  bj-19.41t  37668  bj-0int  38022  orddif0suc  44269  dflim7  44274  mpbiran4d  49907