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  636  mpbiran2d  709  naddcom  8618  naddsuc2  8637  elpmg  8790  letri3  11231  mulsuble0b  12028  xrletri3  13105  qbtwnre  13151  iooneg  13424  invsym  17729  subsubc  17820  lsslss  20956  znleval  21534  psdmvr  22135  restopn2  23142  elflim2  23929  ismet2  24298  mbfi1fseqlem4  25685  deg1ldg  26057  sincosq1sgn  26462  lgsquadlem3  27345  renegscl  28490  numclwwlkqhash  30445  rmounid  32564  dfrdg4  36133  bj-19.41t  37063  bj-0int  37413  orddif0suc  43696  dflim7  43701  mpbiran4d  49273