Theorem baibd 930

Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)

Hypothesis

Ref	Expression
baibd.1	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
baibd	⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃))

Proof of Theorem baibd

Step	Hyp	Ref	Expression
1		baibd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
2		ibar 301	. . 3 ⊢ (𝜒 → (𝜃 ↔ (𝜒 ∧ 𝜃)))
3	2	bicomd 141	. 2 ⊢ (𝜒 → ((𝜒 ∧ 𝜃) ↔ 𝜃))
4	1, 3	sylan9bb 462	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pw2f1odclem  7019  eluz  9768  elicc4  10174  s111  11207  divalgmodcl  12488  eqglact  13811  eqgid  13812  iscrng2  14027  issubrg3  14260  iscld2  14827  cncnp2m  14954  cnnei  14955  reopnap  15269  cnlimc  15395  2omap  16594  pw1map  16596