MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.61ii Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 pm2.61ii.2 . 2 (𝜑𝜒)
2 pm2.61ii.1 . . 3 𝜑 → (¬ 𝜓𝜒))
3 pm2.61ii.3 . . 3 (𝜓𝜒)
42, 3pm2.61d2 181 . 2 𝜑𝜒)
51, 4pm2.61i 182 1 𝜒
Colors of variables: wff setvar class
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  2428  pssnn  9170  pssnnOLD  9267  alephadd  10574  axextnd  10588  axunnd  10593  axpownd  10598  axregndlem2  10600  axregnd  10601  axinfndlem1  10602  axinfnd  10603  2cshwcshw  14780  ressress  17197  frgrreg  29914  bj-hbaeb2  35999  hbae-o  38076  hbequid  38082  ax5eq  38105  ax5el  38110  odd2prm2  46684
  Copyright terms: Public domain W3C validator