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

Theorem ja 189
 Description: Inference joining the antecedents of two premises. For partial converses, see jarri 107 and jarli 126. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 19-Feb-2008.)
Hypotheses
Ref Expression
ja.1 𝜑𝜒)
ja.2 (𝜓𝜒)
Assertion
Ref Expression
ja ((𝜑𝜓) → 𝜒)

Proof of Theorem ja
StepHypRef Expression
1 ja.2 . . 3 (𝜓𝜒)
21imim2i 16 . 2 ((𝜑𝜓) → (𝜑𝜒))
3 ja.1 . 2 𝜑𝜒)
42, 3pm2.61d1 183 1 ((𝜑𝜓) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem is referenced by:  jad  190  pm2.61iOLD  191  pm2.01  192  peirce  205  oibabs  949  pm2.74  972  pm5.71  1025  meredith  1643  tbw-bijust  1700  tbw-negdf  1701  merco1  1715  19.38  1840  19.35  1879  sbi2  2311  sbi2vOLD  2325  sbi2ALT  2608  dfmoeu  2619  moabs  2626  exmoeu  2666  moanimlem  2703  r19.35  3326  elab3gf  3649  r19.2zb  4414  iununi  4994  asymref2  5950  nelaneq  9039  fsuppmapnn0fiub0  13344  itgeq2  24359  frgrwopreglem4a  28073  meran1  33766  imsym1  33773  amosym1  33781  bj-ssbid2ALT  34003  wl-moteq  34797  axc5c7  36085  axc5c711  36092  rp-fakeimass  40015  nanorxor  40792  axc5c4c711  40888  pm2.43cbi  41007  euoreqb  43456
 Copyright terms: Public domain W3C validator