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

Theorem ja 156
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 154 1  |-  ( (
ph  ->  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  jad  157  pm2.61i  159  pm2.01  163  peirce  175  pm2.74  821  oibabs  853  pm5.71  904  dfnot  1342  meredith  1414  tbw-bijust  1473  tbw-negdf  1474  merco1  1488  19.38  1813  hbimOLD  1838  a16gOLD  2050  sbi2  2135  ax46  2241  ax467  2248  mo2  2312  elab3gf  3089  r19.2zb  3720  iununi  4178  asymref2  5254  itgeq2  19672  nbcusgra  21477  wlkntrllem3  21566  meran1  26166  imsym1  26173  amosym1  26181  wl-adnestant  26222  wl-pm5.74lem  26232  ax4567  27592  frgrawopreglem4  28510  pm2.43cbi  28675  a16gNEW7  29620  sbi2NEW7  29638
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator