Theorem pm2.61ii 186

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 184	. 2 ⊢ (¬ 𝜑 → 𝜒)
5	1, 4	pm2.61i 185	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  188  hbae  2430  pssnn  8846  pssnnOLD  8895  alephadd  10191  axextnd  10205  axunnd  10210  axpownd  10215  axregndlem2  10217  axregnd  10218  axinfndlem1  10219  axinfnd  10220  2cshwcshw  14390  ressress  16799  frgrreg  28477  bj-hbaeb2  34738  hbae-o  36654  hbequid  36660  ax5eq  36683  ax5el  36688  odd2prm2  44843