Theorem biancomd 468

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ibar  537  rbaibd  549  pm4.71rd  571  anbi1cd  646  mpbiran2d  720  naddcom  8665  naddsuc2  8684  elpmg  8836  letri3  11290  mulsuble0b  12082  xrletri3  13174  qbtwnre  13220  iooneg  13493  invsym  17814  subsubc  17905  lsslss  21082  znleval  21704  psdmvr  22332  restopn2  23334  elflim2  24121  ismet2  24490  mbfi1fseqlem4  25877  deg1ldg  26249  sincosq1sgn  26663  lgsquadlem3  27546  renegscl  28691  numclwwlkqhash  30726  rmounid  32841  dfrdg4  36443  bj-19.41t  37411  bj-0int  37763  orddif0suc  44015  dflim7  44020  mpbiran4d  49596