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

Theorem ja 174
Description: Inference joining the antecedents of two premises. For partial converses, see jarri 107 and jarli 124. (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 172 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  175  pm2.61i  176  pm2.01  180  peirce  193  oibabs  965  pm2.74  988  pm5.71  1043  meredith  1721  tbw-bijust  1778  tbw-negdf  1779  merco1  1793  19.38  1923  19.35  1967  sbi2  2554  mo2v  2646  exmoeu  2672  moanim  2700  elab3gf  3558  r19.2zb  4263  iununi  4809  asymref2  5731  nelaneq  8746  fsuppmapnn0fiub0  13019  itgeq2  23764  frgrwopreglem4a  27491  meran1  32732  imsym1  32739  amosym1  32747  bj-ssbid2ALT  32966  axc5c7  34692  axc5c711  34699  rp-fakeimass  38358  nanorxor  39005  axc5c4c711  39102  pm2.43cbi  39223
  Copyright terms: Public domain W3C validator