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  2431  pssnn  9168  pssnnOLD  9265  alephadd  10572  axextnd  10586  axunnd  10591  axpownd  10596  axregndlem2  10598  axregnd  10599  axinfndlem1  10600  axinfnd  10601  2cshwcshw  14776  ressress  17193  frgrreg  29647  bj-hbaeb2  35696  hbae-o  37773  hbequid  37779  ax5eq  37802  ax5el  37807  odd2prm2  46386
  Copyright terms: Public domain W3C validator