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

Theorem pm2.61ii 165
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 160 . 2
51, 4pm2.61i 164 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  pm2.61iii  167  hbae  2055  equveliOLD  2089  hbae-o  2232  hbequid  2239  ax5eq  2262  ax5el  2267  pm2.61iineOLD  2780  pssnn  7758  alephadd  8973  axextnd  8987  axunnd  8992  axpowndlem3OLD  8997  axpownd  8999  axregndlem2  9001  axregnd  9002  axregndOLD  9003  axinfndlem1  9004  axinfnd  9005  2cshwcshw  12793  ressress  14694  frgrareg  25117  bj-hbaeb2  34391
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator