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  8669  naddsuc2  8688  elpmg  8840  letri3  11295  mulsuble0b  12087  xrletri3  13179  qbtwnre  13225  iooneg  13498  invsym  17819  subsubc  17910  lsslss  21060  znleval  21673  psdmvr  22301  restopn2  23303  elflim2  24090  ismet2  24459  mbfi1fseqlem4  25846  deg1ldg  26218  sincosq1sgn  26629  lgsquadlem3  27512  renegscl  28657  numclwwlkqhash  30667  rmounid  32782  dfrdg4  36376  bj-19.41t  37314  bj-0int  37665  orddif0suc  43921  dflim7  43926  mpbiran4d  49495