**Description:** Weak deduction theorem eliminating two hypotheses. This theorem is
simpler to use than dedth2v but requires that each hypothesis have
exactly one class variable. See also comments in dedth .
(Contributed by NM, 15-May-1999)

Ref | Expression | ||
---|---|---|---|

Hypotheses | dedth2h.1 | ⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐶 ) → ( 𝜒 ↔ 𝜃 ) ) | |

dedth2h.2 | ⊢ ( 𝐵 = if ( 𝜓 , 𝐵 , 𝐷 ) → ( 𝜃 ↔ 𝜏 ) ) | ||

dedth2h.3 | ⊢ 𝜏 | ||

Assertion | dedth2h | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | dedth2h.1 | ⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐶 ) → ( 𝜒 ↔ 𝜃 ) ) | |

2 | dedth2h.2 | ⊢ ( 𝐵 = if ( 𝜓 , 𝐵 , 𝐷 ) → ( 𝜃 ↔ 𝜏 ) ) | |

3 | dedth2h.3 | ⊢ 𝜏 | |

4 | 1 | imbi2d | ⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐶 ) → ( ( 𝜓 → 𝜒 ) ↔ ( 𝜓 → 𝜃 ) ) ) |

5 | 2 3 | dedth | ⊢ ( 𝜓 → 𝜃 ) |

6 | 4 5 | dedth | ⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) ) |

7 | 6 | imp | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) |