MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ja Unicode version

Theorem ja 153
Description: Inference joining the antecedents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 19-Feb-2008.)
Hypotheses
Ref Expression
ja.1  |-  ( -. 
ph  ->  ch )
ja.2  |-  ( ps 
->  ch )
Assertion
Ref Expression
ja  |-  ( (
ph  ->  ps )  ->  ch )

Proof of Theorem ja
StepHypRef Expression
1 ja.2 . . 3  |-  ( ps 
->  ch )
21imim2i 13 . 2  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ch )
)
3 ja.1 . 2  |-  ( -. 
ph  ->  ch )
42, 3pm2.61d1 151 1  |-  ( (
ph  ->  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  jad  154  pm2.61i  156  pm2.01  160  peirce  172  loolin  173  pm2.74  819  oibabs  851  pm5.71  902  dfnot  1322  meredith  1394  tbw-bijust  1453  tbw-negdf  1454  merco1  1468  hbim  1725  a16g  1885  sbi2  2004  ax46  2101  ax467  2108  mo2  2172  elab3gf  2919  r19.2zb  3544  iununi  3986  asymref2  5060  itgeq2  19132  meran1  24850  imsym1  24857  amosym1  24865  wl-adnestant  24906  wl-pm5.74lem  24917  ax4567  27601  nbcusgra  28159  pm2.43cbi  28280  ax9lem10  29149
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator