This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006)
|
|
Ref |
Expression |
|
Hypothesis |
3anbi1d.1 |
⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) ) |
|
Assertion |
3anbi3d |
⊢ ( 𝜑 → ( ( 𝜃 ∧ 𝜏 ∧ 𝜓 ) ↔ ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
3anbi1d.1 |
⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) ) |
| 2 |
|
biidd |
⊢ ( 𝜑 → ( 𝜃 ↔ 𝜃 ) ) |
| 3 |
2 1
|
3anbi13d |
⊢ ( 𝜑 → ( ( 𝜃 ∧ 𝜏 ∧ 𝜓 ) ↔ ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ) ) |