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  949  pm2.74  972  pm5.71  1025  meredith  1642  tbw-bijust  1699  tbw-negdf  1700  merco1  1714  19.38  1840  19.35  1879  sbi2  2297  dfmoeu  2529  moabs  2536  exmoeu  2574  moanimlem  2613  r19.35  3107  r19.35OLD  3108  r19.21v  3178  elab3gf  3674  elab3g  3675  r19.2zb  4495  ralidmw  4507  ralidm  4511  iununi  5102  asymref2  6118  nelaneq  9600  fsuppmapnn0fiub0  13965  itgeq2  25627  frgrwopreglem4a  29996  meran1  35760  imsym1  35767  bj-ssbid2ALT  36004  wl-moteq  36847  axc5c7  38245  axc5c711  38252  rp-fakeimass  42726  nanorxor  43527  axc5c4c711  43623  pm2.43cbi  43742  euoreqb  46276
  Copyright terms: Public domain W3C validator