Metamath Proof Explorer
Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)
|
|
Ref |
Expression |
|
Hypothesis |
bnj1224.1 |
⊢ ¬ ( 𝜃 ∧ 𝜏 ∧ 𝜂 ) |
|
Assertion |
bnj1224 |
⊢ ( ( 𝜃 ∧ 𝜏 ) → ¬ 𝜂 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1224.1 |
⊢ ¬ ( 𝜃 ∧ 𝜏 ∧ 𝜂 ) |
2 |
|
df-3an |
⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜂 ) ↔ ( ( 𝜃 ∧ 𝜏 ) ∧ 𝜂 ) ) |
3 |
1 2
|
mtbi |
⊢ ¬ ( ( 𝜃 ∧ 𝜏 ) ∧ 𝜂 ) |
4 |
3
|
imnani |
⊢ ( ( 𝜃 ∧ 𝜏 ) → ¬ 𝜂 ) |