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  8648  naddsuc2  8667  elpmg  8818  letri3  11265  mulsuble0b  12061  xrletri3  13120  qbtwnre  13165  iooneg  13438  invsym  17730  subsubc  17821  lsslss  20873  znleval  21470  psdmvr  22062  restopn2  23070  elflim2  23857  ismet2  24227  mbfi1fseqlem4  25625  deg1ldg  26003  sincosq1sgn  26413  lgsquadlem3  27299  renegscl  28355  numclwwlkqhash  30310  rmounid  32430  dfrdg4  35934  bj-19.41t  36757  bj-0int  37084  orddif0suc  43250  dflim7  43255  mpbiran4d  48776