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  8610  naddsuc2  8629  elpmg  8782  letri3  11220  mulsuble0b  12016  xrletri3  13070  qbtwnre  13116  iooneg  13389  invsym  17688  subsubc  17779  lsslss  20914  znleval  21511  psdmvr  22114  restopn2  23123  elflim2  23910  ismet2  24279  mbfi1fseqlem4  25677  deg1ldg  26055  sincosq1sgn  26465  lgsquadlem3  27351  renegscl  28496  numclwwlkqhash  30452  rmounid  32571  dfrdg4  36147  bj-19.41t  36977  bj-0int  37308  orddif0suc  43531  dflim7  43536  mpbiran4d  49064