Theorem biancomd 462

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

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

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 395

This theorem is referenced by:  ibar  527  rbaibd  539  pm4.71rd  561  anbi1cd  632  mpbiran2d  704  naddcom  8683  elpmg  8839  letri3  11303  mulsuble0b  12090  xrletri3  13137  qbtwnre  13182  iooneg  13452  invsym  17713  subsubc  17807  lsslss  20716  znleval  21329  restopn2  22901  elflim2  23688  ismet2  24059  mbfi1fseqlem4  25468  deg1ldg  25845  sincosq1sgn  26244  lgsquadlem3  27121  numclwwlkqhash  29895  rmounid  32002  dfrdg4  35227  bj-19.41t  35955  bj-0int  36285  orddif0suc  42320  dflim7  42325  naddsuc2  42445  mpbiran4d  47570