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

Theorem ja 171
Description: Inference joining the antecedents of two premises. For partial converses, see jarr 103 and jarl 173. (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 169 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  172  pm2.61i  174  pm2.01  178  peirce  191  pm2.74  886  oibabs  920  pm5.71  972  meredith  1556  tbw-bijust  1613  tbw-negdf  1614  merco1  1628  19.38  1755  19.35  1792  sbi2  2376  mo2v  2460  exmoeu  2485  moanim  2512  elab3gf  3320  r19.2zb  4008  iununi  4536  asymref2  5415  fsuppmapnn0fiub0  12606  itgeq2  23263  nbcusgra  25754  wlkntrllem3  25853  frgrawopreglem4  26336  meran1  31382  imsym1  31389  amosym1  31397  bj-ssbid2ALT  31637  axc5c7  33013  axc5c711  33020  rp-fakeimass  36675  nanorxor  37325  axc5c4c711  37423  pm2.43cbi  37544  frgrwopreglem4  41482
  Copyright terms: Public domain W3C validator