Theorem baibr 536

Description: Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)

Hypothesis

Ref	Expression
baib.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
baibr	⊢ (𝜓 → (𝜒 ↔ 𝜑))

Proof of Theorem baibr

Step	Hyp	Ref	Expression
1		baib.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	baib 535	. 2 ⊢ (𝜓 → (𝜑 ↔ 𝜒))
3	2	bicomd 223	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:  rbaibr  537  pm5.44  542  exmoeub  2581  ssnelpss  4055  brinxp  5704  copsex2ga  5757  canth  7315  riotaxfrd  7352  iscard  9893  kmlem14  10080  ltxrlt  11210  elioo5  13350  prmind2  16648  pcelnn  16835  isnirred  20394  isdomn3  20686  isreg2  23355  comppfsc  23510  kqcldsat  23711  elmptrab  23805  itg2uba  25723  prmorcht  27158  adjeq  32024  lnopcnbd  32125  cvexchlem  32457  maprnin  32822  topfne  36555  ismblfin  37999  ftc1anclem5  38035  isdmn2  38393  cdlemefrs29pre00  40858  cdlemefrs29cpre1  40861  elmapintab  44044  bits0ALTV  48170