Description: Hypothesis builder for the weak deduction theorem. For more information, see the Weak Deduction Theorem page mmdeduction.html . (Contributed by NM, 26-Jun-2002) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019) Commute consequent. (Revised by Steven Nguyen, 27-Apr-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | elimh.1 | ⊢ ( ( if- ( 𝜒 , 𝜑 , 𝜓 ) ↔ 𝜑 ) → ( 𝜏 ↔ 𝜒 ) ) | |
| elimh.2 | ⊢ ( ( if- ( 𝜒 , 𝜑 , 𝜓 ) ↔ 𝜓 ) → ( 𝜏 ↔ 𝜃 ) ) | ||
| elimh.3 | ⊢ 𝜃 | ||
| Assertion | elimh | ⊢ 𝜏 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elimh.1 | ⊢ ( ( if- ( 𝜒 , 𝜑 , 𝜓 ) ↔ 𝜑 ) → ( 𝜏 ↔ 𝜒 ) ) | |
| 2 | elimh.2 | ⊢ ( ( if- ( 𝜒 , 𝜑 , 𝜓 ) ↔ 𝜓 ) → ( 𝜏 ↔ 𝜃 ) ) | |
| 3 | elimh.3 | ⊢ 𝜃 | |
| 4 | ifptru | ⊢ ( 𝜒 → ( if- ( 𝜒 , 𝜑 , 𝜓 ) ↔ 𝜑 ) ) | |
| 5 | 4 1 | syl | ⊢ ( 𝜒 → ( 𝜏 ↔ 𝜒 ) ) |
| 6 | 5 | ibir | ⊢ ( 𝜒 → 𝜏 ) |
| 7 | ifpfal | ⊢ ( ¬ 𝜒 → ( if- ( 𝜒 , 𝜑 , 𝜓 ) ↔ 𝜓 ) ) | |
| 8 | 7 2 | syl | ⊢ ( ¬ 𝜒 → ( 𝜏 ↔ 𝜃 ) ) |
| 9 | 3 8 | mpbiri | ⊢ ( ¬ 𝜒 → 𝜏 ) |
| 10 | 6 9 | pm2.61i | ⊢ 𝜏 |