Theorem 3anbi13d 899

Description: Deduction conjoining and adding a conjunct to equivalences.

Hypotheses

Ref	Expression
3anbi12d.1	⊢ (φ → (ψ ↔ χ))
3anbi12d.2	⊢ (φ → (θ ↔ τ))

Assertion

Ref	Expression
3anbi13d	⊢ (φ → ((ψ ⋀ η ⋀ θ) ↔ (χ ⋀ η ⋀ τ)))

Proof of Theorem 3anbi13d

Step	Hyp	Ref	Expression
1		3anbi12d.1	. 2 ⊢ (φ → (ψ ↔ χ))
2		pm4.2d 171	. 2 ⊢ (φ → (η ↔ η))
3		3anbi12d.2	. 2 ⊢ (φ → (θ ↔ τ))
4	1, 2, 3	3anbi123d 897	1 ⊢ (φ → ((ψ ⋀ η ⋀ θ) ↔ (χ ⋀ η ⋀ τ)))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ w3a 779

This theorem is referenced by:  3anbi3d 903  bcpasc2 7000  methausi 7907  metdnsconst 7927  lmbr 7954  iscau3 7964  iscau4 7966  isnvlem 8254  nvi 8258  adjval 9838  adj1 9881  adjeq 9883  cnlnssadj 10037  hmph 10557  fillsb 10593  dtt2 10636  isded 10690  dedi 10691  ismonb2 10761  isepib2 10771

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 781

Copyright terms: Public domain