This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1241

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1241.1 ⊢ φ → A ⊆ B
bnj1241.2 ⊢ ψ → C = A
Assertion bnj1241 ⊢ φ ∧ ψ → C ⊆ B

Proof

Step Hyp Ref Expression
1 bnj1241.1 ⊢ φ → A ⊆ B
2 bnj1241.2 ⊢ ψ → C = A
3 2 eqcomd ⊢ ψ → A = C
4 3 adantl ⊢ φ ∧ ψ → A = C
5 1 adantr ⊢ φ ∧ ψ → A ⊆ B
6 4 5 eqsstrrd ⊢ φ ∧ ψ → C ⊆ B