Theorem biancomd 467

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  ibar  536  rbaibd  548  pm4.71rd  570  anbi1cd  644  mpbiran2d  718  naddcom  8653  naddsuc2  8672  elpmg  8824  letri3  11268  mulsuble0b  12064  xrletri3  13156  qbtwnre  13202  iooneg  13475  invsym  17795  subsubc  17886  lsslss  21028  znleval  21606  psdmvr  22234  restopn2  23237  elflim2  24024  ismet2  24393  mbfi1fseqlem4  25780  deg1ldg  26152  sincosq1sgn  26563  lgsquadlem3  27446  renegscl  28591  numclwwlkqhash  30577  rmounid  32694  dfrdg4  36301  bj-19.41t  37241  bj-0int  37591  orddif0suc  43845  dflim7  43850  mpbiran4d  49419