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

Theorem pm2.61ii 160
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 155 . 2  |-  ( -. 
ph  ->  ch )
51, 4pm2.61i 159 1  |-  ch
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.61iii  162  hbae  2041  hbaeOLD  2042  equveli  2086  sbequi  2111  sbequiOLD  2115  sbcom  2165  sbcomOLD  2166  sbcom2  2191  hbae-o  2231  hbequid  2238  ax17eq  2261  ax17el  2267  pssnn  7328  alephadd  8453  axextnd  8467  axunnd  8472  axpowndlem3  8475  axpownd  8477  axregndlem2  8479  axregnd  8480  axinfndlem1  8481  axinfnd  8482  ressress  13527  pm2.61iine  25187  hbaewAUX7  29479  sbequiNEW7  29580  sbcomwAUX7  29589  sbcom2NEW7  29645  hbaew0AUX7  29648  hbaeOLD7  29709  sbcomOLD7  29756
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator