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

Theorem pm2.61ii 168
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  |-  ( -. 
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 163 . 2  |-  ( -. 
ph  ->  ch )
51, 4pm2.61i 167 1  |-  ch
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  170  hbae  2110  pm2.61iineOLD  2747  pssnn  7792  alephadd  9002  axextnd  9016  axunnd  9021  axpownd  9026  axregndlem2  9028  axregnd  9029  axinfndlem1  9030  axinfnd  9031  2cshwcshw  12912  ressress  15172  frgrareg  25828  bj-hbaeb2  31375  hbae-o  32389  hbequid  32396  ax5eq  32419  ax5el  32424
  Copyright terms: Public domain W3C validator