New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  pm2.61da3ne GIF version

Theorem pm2.61da3ne 2596
 Description: Deduction eliminating three inequalities in an antecedent. (Contributed by NM, 15-Jun-2013.)
Hypotheses
Ref Expression
pm2.61da3ne.1 ((φ A = B) → ψ)
pm2.61da3ne.2 ((φ C = D) → ψ)
pm2.61da3ne.3 ((φ E = F) → ψ)
pm2.61da3ne.4 ((φ (AB CD EF)) → ψ)
Assertion
Ref Expression
pm2.61da3ne (φψ)

Proof of Theorem pm2.61da3ne
StepHypRef Expression
1 pm2.61da3ne.1 . 2 ((φ A = B) → ψ)
2 pm2.61da3ne.2 . 2 ((φ C = D) → ψ)
3 pm2.61da3ne.3 . . . 4 ((φ E = F) → ψ)
43adantlr 695 . . 3 (((φ (AB CD)) E = F) → ψ)
5 simpll 730 . . . 4 (((φ (AB CD)) EF) → φ)
6 simplrl 736 . . . 4 (((φ (AB CD)) EF) → AB)
7 simplrr 737 . . . 4 (((φ (AB CD)) EF) → CD)
8 simpr 447 . . . 4 (((φ (AB CD)) EF) → EF)
9 pm2.61da3ne.4 . . . 4 ((φ (AB CD EF)) → ψ)
105, 6, 7, 8, 9syl13anc 1184 . . 3 (((φ (AB CD)) EF) → ψ)
114, 10pm2.61dane 2594 . 2 ((φ (AB CD)) → ψ)
121, 2, 11pm2.61da2ne 2595 1 (φψ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358   ∧ w3a 934   = wceq 1642   ≠ wne 2516 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-ne 2518 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator