New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  ja GIF version

Theorem ja 153
 Description: Inference joining the antecedents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by 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 13 . 2 ((φψ) → (φχ))
3 ja.1 . 2 φχ)
42, 3pm2.61d1 151 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  154  pm2.61i  156  pm2.01  160  peirce  172  loolin  173  pm2.74  819  oibabs  851  pm5.71  902  dfnot  1332  meredith  1404  tbw-bijust  1463  tbw-negdf  1464  merco1  1478  19.38  1794  hbimOLD  1818  a16g  1945  sbi2  2064  ax46  2162  ax467  2169  mo2  2233  elab3gf  2990  r19.2zb  3640  iununi  4050
 Copyright terms: Public domain W3C validator