MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.61ii Structured version   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  |-  ( -. 
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 160 . 2  |-  ( -. 
ph  ->  ch )
51, 4pm2.61i 164 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  167  hbae  2012  equveliOLD  2046  sbcom2OLD  2159  hbae-o  2210  hbequid  2217  ax5eq  2240  ax5el  2245  pm2.61iineOLD  2771  pssnn  7634  alephadd  8844  axextnd  8858  axunnd  8863  axpowndlem3OLD  8868  axpownd  8870  axregndlem2  8872  axregnd  8873  axregndOLD  8874  axinfndlem1  8875  axinfnd  8876  ressress  14339  cshwlemma1  30629  frgrareg  30850
  Copyright terms: Public domain W3C validator