MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ja Structured version   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  1341  meredith  1413  tbw-bijust  1472  tbw-negdf  1473  merco1  1487  19.38  1812  hbimOLD  1837  a16gOLD  2049  sbi2  2120  ax46  2238  ax467  2245  mo2  2309  elab3gf  3079  r19.2zb  3710  iununi  4167  asymref2  5243  itgeq2  19661  nbcusgra  21464  wlkntrllem3  21553  meran1  26153  imsym1  26160  amosym1  26168  wl-adnestant  26209  wl-pm5.74lem  26219  ax4567  27569  frgrawopreglem4  28373  pm2.43cbi  28538  a16gNEW7  29483  sbi2NEW7  29501
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator