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  2028  equveliOLD  2062  sbcom2OLD  2174  hbae-o  2225  hbequid  2232  ax5eq  2255  ax5el  2260  pm2.61iineOLD  2790  pssnn  7750  alephadd  8964  axextnd  8978  axunnd  8983  axpowndlem3OLD  8988  axpownd  8990  axregndlem2  8992  axregnd  8993  axregndOLD  8994  axinfndlem1  8995  axinfnd  8996  2cshwcshw  12773  ressress  14569  frgrareg  24941  bj-hbaeb2  33873
  Copyright terms: Public domain W3C validator