Theorem bi2anan9 478

Description: Deduction joining two equivalences to form equivalence of conjunctions.

Hypotheses

Ref	Expression
bi2an9.1	⊢ (φ → (ψ ↔ χ))
bi2an9.2	⊢ (θ → (τ ↔ η))

Assertion

Ref	Expression
bi2anan9	⊢ ((φ ∧ θ) → ((ψ ∧ τ) ↔ (χ ∧ η)))

Proof of Theorem bi2anan9

Step	Hyp	Ref	Expression
1		bi2an9.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2	1	anbi1d 469	. 2 ⊢ (φ → ((ψ ∧ τ) ↔ (χ ∧ τ)))
3		bi2an9.2	. . 3 ⊢ (θ → (τ ↔ η))
4	3	anbi2d 468	. 2 ⊢ (θ → ((χ ∧ τ) ↔ (χ ∧ η)))
5	2, 4	sylan9bb 418	1 ⊢ ((φ ∧ θ) → ((ψ ∧ τ) ↔ (χ ∧ η)))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196

This theorem is referenced by:  bi2anan9r 479  copsex4g 1904  cleqrel 2483  f1fv 2916  oprabval4g 3053  th3qlem1 3250  th3qlem2 3251  oprec 3254  unen 3338  endisj 3341  aceq5lem4 3561  ordpipq 3850  genpv 3896  genpprecl 3898  distrlem5pr 3925  ltsrpr 3980  axcnre 4087  lt2sq 4414

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org