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

Theorem ja 155
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 14 . 2  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ch )
)
3 ja.1 . 2  |-  ( -. 
ph  ->  ch )
42, 3pm2.61d1 153 1  |-  ( (
ph  ->  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  jad  156  pm2.61i  158  pm2.01  162  peirce  174  pm2.74  820  oibabs  852  pm5.71  903  dfnot  1338  meredith  1410  tbw-bijust  1469  tbw-negdf  1470  merco1  1484  19.38  1802  hbimOLD  1827  a16g  1977  sbi2  2090  ax46  2189  ax467  2196  mo2  2260  elab3gf  3023  r19.2zb  3654  iununi  4109  asymref2  5184  itgeq2  19529  nbcusgra  21331  wlkntrllem5  21410  meran1  25868  imsym1  25875  amosym1  25883  wl-adnestant  25924  wl-pm5.74lem  25934  ax4567  27263  frgrawopreglem4  27792  pm2.43cbi  27937  a16gNEW7  28875  sbi2NEW7  28893  ax9lem10  29125
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator