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  8951  pssnnOLD  9040  alephadd  10333  axextnd  10347  axunnd  10352  axpownd  10357  axregndlem2  10359  axregnd  10360  axinfndlem1  10361  axinfnd  10362  2cshwcshw  14538  ressress  16958  frgrreg  28758  bj-hbaeb2  35001  hbae-o  36917  hbequid  36923  ax5eq  36946  ax5el  36951  odd2prm2  45170