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  8646  naddsuc2  8665  elpmg  8816  letri3  11259  mulsuble0b  12055  xrletri3  13114  qbtwnre  13159  iooneg  13432  invsym  17724  subsubc  17815  lsslss  20867  znleval  21464  psdmvr  22056  restopn2  23064  elflim2  23851  ismet2  24221  mbfi1fseqlem4  25619  deg1ldg  25997  sincosq1sgn  26407  lgsquadlem3  27293  renegscl  28349  numclwwlkqhash  30304  rmounid  32424  dfrdg4  35939  bj-19.41t  36762  bj-0int  37089  orddif0suc  43257  dflim7  43262  mpbiran4d  48786