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  8612  naddsuc2  8631  elpmg  8784  letri3  11225  mulsuble0b  12022  xrletri3  13099  qbtwnre  13145  iooneg  13418  invsym  17723  subsubc  17814  lsslss  20950  znleval  21547  psdmvr  22148  restopn2  23155  elflim2  23942  ismet2  24311  mbfi1fseqlem4  25698  deg1ldg  26070  sincosq1sgn  26478  lgsquadlem3  27362  renegscl  28507  numclwwlkqhash  30463  rmounid  32582  dfrdg4  36152  bj-19.41t  37082  bj-0int  37432  orddif0suc  43717  dflim7  43722  mpbiran4d  49288