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

Theorem ja 186
Description: Inference joining the antecedents of two premises. For partial converses, see jarri 107 and jarli 126. (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 180 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  187  pm2.01  188  peirce  201  oibabs  951  pm2.74  974  pm5.71  1027  meredith  1644  tbw-bijust  1701  tbw-negdf  1702  merco1  1716  19.38  1842  19.35  1881  sbi2  2299  dfmoeu  2535  moabs  2542  exmoeu  2580  moanimlem  2619  r19.35  3112  r19.35OLD  3113  r19.21v  3177  elab3gf  3637  elab3g  3638  r19.2zb  4454  ralidmw  4466  ralidm  4470  iununi  5060  asymref2  6072  nelaneq  9536  fsuppmapnn0fiub0  13899  itgeq2  25145  frgrwopreglem4a  29257  meran1  34886  imsym1  34893  bj-ssbid2ALT  35130  wl-moteq  35976  axc5c7  37376  axc5c711  37383  rp-fakeimass  41791  nanorxor  42592  axc5c4c711  42688  pm2.43cbi  42807  euoreqb  45348
  Copyright terms: Public domain W3C validator