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  1893  sbequi  1999  sbcom  2029  sbcom2  2053  hbae-o  2092  hbequid  2099  ax17eq  2122  ax17el  2128  pssnn  7081  alephadd  8199  axextnd  8213  axunnd  8218  axpowndlem3  8221  axpownd  8223  axregndlem2  8225  axregnd  8226  axinfndlem1  8227  axinfnd  8228  ressress  13205  pm2.61iine  24081
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator