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  635  mpbiran2d  708  naddcom  8608  naddsuc2  8627  elpmg  8778  letri3  11216  mulsuble0b  12012  xrletri3  13066  qbtwnre  13112  iooneg  13385  invsym  17684  subsubc  17775  lsslss  20910  znleval  21507  psdmvr  22110  restopn2  23119  elflim2  23906  ismet2  24275  mbfi1fseqlem4  25673  deg1ldg  26051  sincosq1sgn  26461  lgsquadlem3  27347  renegscl  28443  numclwwlkqhash  30399  rmounid  32518  dfrdg4  36094  bj-19.41t  36918  bj-0int  37245  orddif0suc  43452  dflim7  43457  mpbiran4d  48985