**Description:** Deduction eliminating two inequalities in an antecedent. (Contributed by NM, 29-May-2013)

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

Hypotheses | pm2.61da2ne.1 | ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝜓 ) | |

pm2.61da2ne.2 | ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐷 ) → 𝜓 ) | ||

pm2.61da2ne.3 | ⊢ ( ( 𝜑 ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ) ) → 𝜓 ) | ||

Assertion | pm2.61da2ne | ⊢ ( 𝜑 → 𝜓 ) |

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

1 | pm2.61da2ne.1 | ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝜓 ) | |

2 | pm2.61da2ne.2 | ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐷 ) → 𝜓 ) | |

3 | pm2.61da2ne.3 | ⊢ ( ( 𝜑 ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ) ) → 𝜓 ) | |

4 | 2 | adantlr | ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐶 = 𝐷 ) → 𝜓 ) |

5 | 3 | anassrs | ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐷 ) → 𝜓 ) |

6 | 4 5 | pm2.61dane | ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝜓 ) |

7 | 1 6 | pm2.61dane | ⊢ ( 𝜑 → 𝜓 ) |