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

Theorem ja 173
 Description: Inference joining the antecedents of two premises. For partial converses, see jarr 106 and jarl 175. (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 171 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  174  pm2.61i  176  pm2.01  180  peirce  193  pm2.74  890  oibabs  924  pm5.71  976  meredith  1564  tbw-bijust  1621  tbw-negdf  1622  merco1  1636  19.38  1764  19.35  1803  sbi2  2391  mo2v  2475  exmoeu  2500  moanim  2527  elab3gf  3350  r19.2zb  4052  iununi  4601  asymref2  5501  fsuppmapnn0fiub0  12776  itgeq2  23525  frgrwopreglem4  27157  meran1  32385  imsym1  32392  amosym1  32400  bj-ssbid2ALT  32621  axc5c7  34015  axc5c711  34022  rp-fakeimass  37676  nanorxor  38324  axc5c4c711  38422  pm2.43cbi  38544
 Copyright terms: Public domain W3C validator