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  1737  a16g  1898  sbi2  2017  ax46  2114  ax467  2121  mo2  2185  elab3gf  2932  r19.2zb  3557  iununi  4002  asymref2  5076  itgeq2  19148  meran1  24922  imsym1  24929  amosym1  24937  wl-adnestant  24978  wl-pm5.74lem  24989  ax4567  27704  nbcusgra  28298  wlkntrllem5  28349  pm2.43cbi  28579  a16gNEW7  29521  sbi2NEW7  29539  ax9lem10  29771
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator