Theorem pm2.61ii 183

Description: Inference eliminating two antecedents. (Contributed by NM, 4-Jan-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)

Hypotheses

Ref	Expression
pm2.61ii.1	⊢ (¬ 𝜑 → (¬ 𝜓 → 𝜒))
pm2.61ii.2	⊢ (𝜑 → 𝜒)
pm2.61ii.3	⊢ (𝜓 → 𝜒)

Assertion

Ref	Expression
pm2.61ii	⊢ 𝜒

Proof of Theorem pm2.61ii

Step	Hyp	Ref	Expression
1		pm2.61ii.2	. 2 ⊢ (𝜑 → 𝜒)
2		pm2.61ii.1	. . 3 ⊢ (¬ 𝜑 → (¬ 𝜓 → 𝜒))
3		pm2.61ii.3	. . 3 ⊢ (𝜓 → 𝜒)
4	2, 3	pm2.61d2 181	. 2 ⊢ (¬ 𝜑 → 𝜒)
5	1, 4	pm2.61i 182	1 ⊢ 𝜒

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  pm2.61iii  185  hbae  2431  pssnn  8913  pssnnOLD  8969  alephadd  10264  axextnd  10278  axunnd  10283  axpownd  10288  axregndlem2  10290  axregnd  10291  axinfndlem1  10292  axinfnd  10293  2cshwcshw  14466  ressress  16884  frgrreg  28659  bj-hbaeb2  34928  hbae-o  36844  hbequid  36850  ax5eq  36873  ax5el  36878  odd2prm2  45058