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  634  mpbiran2d  707  naddcom  8734  naddsuc2  8753  elpmg  8897  letri3  11371  mulsuble0b  12163  xrletri3  13212  qbtwnre  13257  iooneg  13527  invsym  17818  subsubc  17912  lsslss  20977  znleval  21591  restopn2  23199  elflim2  23986  ismet2  24357  mbfi1fseqlem4  25766  deg1ldg  26143  sincosq1sgn  26550  lgsquadlem3  27435  renegscl  28439  numclwwlkqhash  30398  rmounid  32514  dfrdg4  35907  bj-19.41t  36688  bj-0int  37015  orddif0suc  43170  dflim7  43175  mpbiran4d  48449