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  8609  naddsuc2  8628  elpmg  8781  letri3  11220  mulsuble0b  12017  xrletri3  13094  qbtwnre  13140  iooneg  13413  invsym  17718  subsubc  17809  lsslss  20945  znleval  21542  psdmvr  22144  restopn2  23151  elflim2  23938  ismet2  24307  mbfi1fseqlem4  25694  deg1ldg  26069  sincosq1sgn  26478  lgsquadlem3  27364  renegscl  28509  numclwwlkqhash  30465  rmounid  32584  dfrdg4  36154  bj-19.41t  37076  bj-0int  37426  orddif0suc  43711  dflim7  43716  mpbiran4d  49270