Theorem biancomd 464

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 461	. 2 ⊢ ((𝜃 ∧ 𝜒) ↔ (𝜒 ∧ 𝜃))
3	1, 2	bitrdi 287	1 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  ibar  529  rbaibd  541  pm4.71rd  563  anbi1cd  634  mpbiran2d  705  elpmg  8631  letri3  11060  mulsuble0b  11847  xrletri3  12888  qbtwnre  12933  iooneg  13203  invsym  17474  subsubc  17568  lsslss  20223  znleval  20762  restopn2  22328  elflim2  23115  ismet2  23486  mbfi1fseqlem4  24883  deg1ldg  25257  sincosq1sgn  25655  lgsquadlem3  26530  numclwwlkqhash  28739  rmounid  30843  naddcom  33835  dfrdg4  34253  bj-19.41t  34956  bj-0int  35272  mpbiran4d  46143