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  927  oibabs  961  pm5.71  1015  meredith  1715  tbw-bijust  1772  tbw-negdf  1773  merco1  1787  19.38  1915  19.35  1954  sbi2  2530  mo2v  2614  exmoeu  2640  moanim  2667  elab3gf  3496  r19.2zb  4205  iununi  4762  asymref2  5671  nelaneq  8671  fsuppmapnn0fiub0  13007  itgeq2  23763  frgrwopreglem4a  27485  meran1  32737  imsym1  32744  amosym1  32752  bj-ssbid2ALT  32974  axc5c7  34718  axc5c711  34725  rp-fakeimass  38377  nanorxor  39024  axc5c4c711  39122  pm2.43cbi  39244
 Copyright terms: Public domain W3C validator