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  1808  hbimOLD  1833  a16gOLD  2013  sbi2  2113  ax46  2212  ax467  2219  mo2  2283  elab3gf  3047  r19.2zb  3678  iununi  4135  asymref2  5210  itgeq2  19622  nbcusgra  21425  wlkntrllem3  21514  meran1  26065  imsym1  26072  amosym1  26080  wl-adnestant  26121  wl-pm5.74lem  26131  ax4567  27469  frgrawopreglem4  28150  pm2.43cbi  28312  a16gNEW7  29250  sbi2NEW7  29268
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator