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

Theorem pm2.61ii 157
Description: Inference eliminating two antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
Hypotheses
Ref Expression
pm2.61ii.1  |-  ( -. 
ph  ->  ( -.  ps  ->  ch ) )
pm2.61ii.2  |-  ( ph  ->  ch )
pm2.61ii.3  |-  ( ps 
->  ch )
Assertion
Ref Expression
pm2.61ii  |-  ch

Proof of Theorem pm2.61ii
StepHypRef Expression
1 pm2.61ii.2 . 2  |-  ( ph  ->  ch )
2 pm2.61ii.1 . . 3  |-  ( -. 
ph  ->  ( -.  ps  ->  ch ) )
3 pm2.61ii.3 . . 3  |-  ( ps 
->  ch )
42, 3pm2.61d2 152 . 2  |-  ( -. 
ph  ->  ch )
51, 4pm2.61i 156 1  |-  ch
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.61iii  159  hbae  1906  sbequi  2012  sbcom  2042  sbcom2  2066  hbae-o  2105  hbequid  2112  ax17eq  2135  ax17el  2141  pssnn  7097  alephadd  8215  axextnd  8229  axunnd  8234  axpowndlem3  8237  axpownd  8239  axregndlem2  8241  axregnd  8242  axinfndlem1  8243  axinfnd  8244  ressress  13221  pm2.61iine  24096  hbaewAUX7  29455  sbequiNEW7  29553  sbcomwAUX7  29562  hbaew0AUX7  29617  hbaeOLD7  29662  sbcomOLD7  29709  sbcom2OLD7  29715
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator