MPE Home 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  1563  tbw-bijust  1620  tbw-negdf  1621  merco1  1635  19.38  1763  19.35  1802  sbi2  2392  mo2v  2476  exmoeu  2501  moanim  2528  elab3gf  3344  r19.2zb  4039  iununi  4583  asymref2  5482  fsuppmapnn0fiub0  12749  itgeq2  23484  frgrwopreglem4  27076  meran1  32105  imsym1  32112  amosym1  32120  bj-ssbid2ALT  32341  axc5c7  33715  axc5c711  33722  rp-fakeimass  37377  nanorxor  38025  axc5c4c711  38123  pm2.43cbi  38245
  Copyright terms: Public domain W3C validator